11.4. Invariants

A class invariant is a condition that should never be violated in any object, after it has been created. Invariants have not proven to be as widely used as pre- and post- conditions, which are quite ubiquitous in Sather code.

11.4.1. The invariant routine

If a routine with the signature 'invariant:BOOL', appears in a class, it defines a class invariant. It is a fatal error for it to evaluate to false after any public method of the class returns, yields, or quits.

Consider a class with a list (we use the library class A_LIST) whose size must always be at least 1. Such a situtation could arise if the array usually contains the same sort of elements and we want to use the first element of the array as a prototypical element)
class PROTO_LIST is
   private attr l:A_LIST{FOO};

   create(first_elt:FOO):SAME is
      res ::= new;
      res.l := #;
      return res;

   invariant:BOOL is
      return l.size > 0

   delete_last:FOO is
      return l.delete_elt(l.size-1);

If the 'delete_last' operation is called on the last element, then the assertion will be violated and an error will result.
proto:FOO := #;   -- Some FOO object
last:FOO := a.delete_last;
   -- At runtime, an invariant violation will occur
   -- for trying to remove the last element.

The invariant is checked at the end of every public method. However, the invariant is not checked after a private routine. If we have the additional routines
delete_and_add is
   res ::= internal_delete_last;
   return res;

private internal_delete_last:FOO is
   return l.delete_elt(l.size-1);

Now we can call 'delete_and_add'
proto:FOO := #;
last:FOO := a.delete_and_add;  -- does not violate the class invariant

The private call to 'internal_delete_last' does violate the invariant, but it is not checked, since it is a private routine.