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.
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 := #;
res.l.append(first_elt);
return res;
end;
invariant:BOOL is
return l.size > 0
end;
delete_last:FOO is
return l.delete_elt(l.size-1);
end;
end; |
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 a:PROTO_LIST := #(FOO); 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; l.append(res); return res; end; private internal_delete_last:FOO is return l.delete_elt(l.size-1); end; |
Now we can call 'delete_and_add'
proto:FOO := #; a:PROTO_LIST := #(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.