Ring concept

Description

A ring is an algebraic structure that is a abelian group for the addition with a multiplication operator '*' such that

Refinement of

AdditiveAbelianGroup

Notation

X type that is a model of Field
a, b Object of type X
0 Zero element: identity for addition
1 One element: identity for multiplication

Definitions

Valid expressions

In addition to those defined by AdditiveAbelianGroup:
Name Expression Return type
One element one( a ) void
Multiplication a * b X
Multiplication assignment a *= b X

Expression semantics

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

Complexity guarantees

Invariants

Commutativity for Addition a + b = b + a
Commutativity for Multiplication a * b = b * a
Negation (-a) + a = 0 and a-a = 0

Models

Notes