MultiplicativeGroup concept

Description

An AdditiveGroup (denoted as (G,*)) is a Group with the multiplication (*) as operator.

For an MultiplicativeGroup

Refinement of

Group.

Notation

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

Definitions

Valid expressions

In addition to those defined by Group
Name Expression Return type
Identity element one(a) void
Multiplication a * b X
Division a / b X
Multiplication assignment a *= b X
Division assignment a /= b X

Expression semantics

Name Expression Precondition Semantics Postcondition
One element one(a)   Set a to the identity element (1)  
Multiplication a * b      
Division a / b   equivalent to a * (1/b)  
Multiplication assignment a *= b   equivalent to a = a * b  
Division assignment a /= b   equivalent to a = a / b  

Complexity guarantees

Invariants

Inherited from Group.

Models

Notes