AdditiveAbelianGroup concept

Description

An AddititiveAbelianGroup is an AbelianGroup equipped with the addition (+) operator.

Refinement of

AbelianGroup and AdditiveGroup.

Notation

X type that is a model of Group
a, b Object of type X
0 Zero element: identity element for addition

Definitions

Valid expressions

None in addition to those defined by AdditiveGroup.

Expression semantics

Name Expression Precondition Semantics Postcondition

Complexity guarantees

Invariants

Models

Notes