Re: Making guarantees about record components

[tmoran@acm.org]

> To really guarantee the property, you'd have to encapsulate M ...
  How many bugs have been caused by things like leaving out the first
line of
  Last := Last+1;
  Saved(Last) := New_Item;
(or misplacing the "++" in C code).
 The only way to ensure the abstraction of a data structure where Last
always points to the last item in Saved is by hiding it and
introducing an Append procedure.  For simple abstractions like this,
that's so heavy handed it's rarely done.  Predicates, as in the OP's
problem, are a very limited step toward eliminating this class of errors.