AdditiveGroup concept

Description

An AdditiveGroup (denoted as (G,+)) is a Group with the addition (+) as operator.

For an AdditiveGroup

Refinement of

Group.

Notation

X type that is a model of Group
a, b Object of type X
0 identity element

Definitions

Valid expressions

In addition to those defined by Group
Name Expression Return type
Identity element zero(a) void
Addition a + b X
Subtraction a - b X
Addition assignment a += b X
Subtraction assignment a -= b X
Negation -a X

Expression semantics

Name Expression Precondition Semantics Postcondition
Zero element zero(a)   Set a to the zero element (0)  
Addition a + b      
Subtraction a - b   equivalent to a + (-b)  
Addition assignment a += b   equivalent to a = a + b  
Subtraction assignment a -= b   equivalent to a += -b  
Negation -a   Equivalent to 0 - a  

Complexity guarantees

Invariants

Inherited from Group.

Models

Notes