Group concept

Description

A group is an algebraic structure on a finite or infinite set equipped with an operator (in the following we use the notation '@' for the operator).

Let a and b be arbitrary elements of the group. The following properties hold:

Refinement of

Assignable, DefaultConstructible and EqualityComparable.

Notation

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

Definitions

Valid expressions

In addition to those defined by Assignable, DefaultConstructible and EqualityComparable:
Name Expression Return type

Expression semantics

Name Expression Precondition Semantics Postcondition

Complexity guarantees

Invariants

Inversion a @ b = e

Models

Notes