Constraints

From dis-Emi-A

Contraints are the more general form of Constrained Types. Unlike types however they may appear anywhat in the code and establish rules by which the code is expected to operator. They are strictly unnecessary but singificantly aid in finding defects in the code.

Types

There are several types of constraints that can be used.

Contrained Types 

constraints applied to specific variables or types

Invariants 

constraints that must always be true

Assumptions / preconditions 

constraints which must be met before a section of code can execute or on which a section of code relies

Effects / postconditions 

contraints which must be met upon completion of a section of code

Static constraints 

these are really the basis for unit testing but allow specifying of small conditionds directly near the related code.

Examples

In quasi syntax (as not enough syntax has yet been defined) based on C++:

class Bag
{
  maxSize = 50;
  set backingSet;
    @( backingSet.size <= maxSize )

  PlaceInBag( a )
    @( a.weight <= maxWeight )
    {
    backingSet = backingSet ++ a; //concatenate a to set
    }
    @( backingSet contains a )
}

Note the relation to constrained types as the set above could have also been declared without the invariant and rather as a constrained type:

set : size <= maxSize : backingSet;

Though, we have to determine whether constraints can refer to local or class variables, this may make compilation too difficult (though difficulty of compilation is not our topmost goal).