Re: Specifying the order of ops on an ADT with aspects

["Hibou57 (Yannick Duchêne)" <yannick_duchene@yahoo.fr>]

Side comment.

There is another good side effect of pre-post-conditions, apart their
abilities to better express contracts and to check usages and
implementations conformance : as you define pre-post-conditions, you
see what's needed to define these, so it enforce completeness of ADTs.
With this kind of design, one is less likely to miss a required
function to test an instance of an ADT. Last and although indirectly,
these functions, in turn sometimes makes the need of some associated
procedures more clear.

This is an aid in setting up specifications.