The concept Regular is the basic concept which allows for equational reasoning about code. Each of the sub-concepts which it refines are interconnected by the axioms which cannot be expressed until combined here.
- Valid Expressions:
- All expressions that match the above concepts are valid.
- Expression Semantics:
- Given type
Twhich models Regular and an action
zap()which always modifies it's parameter:
T a = b; assert(a == b);copies are equal
T a; a = b;is equivalent to
T a(b);relate copy and assignment
T a = c; T b = c; a = d; assert(b==c);copies are disjoint
T a = c; T b = c; zap(a); assert(b==c && a!=b);copies don't intersect
- Type(s) Modeling this Concept: