Re: Question on type invariants

["Randy Brukardt" <randy@rrsoftware.com>]

"reinkor" <reinkor@gmail.com> wrote in message 
news:65f79e53-a468-4b77-8ee1-440c26a09371@googlegroups.com...
...
> I can program the whole thing and keep the concepts in my head, but is it 
> a natural
>"Ada way" to secure that S is up-to-date when used? Is "type invariants" of 
>any help?

Perhaps, if you can only export up-to-date versions of S. Type invariants 
are (mostly) enforced at the package boundary, that is when objects are 
passed in and out of the package that implements S.

I generally find that type invariants are too limiting. It's usually easier 
to have a dynamic predicate on a subtype; you can then apply that subtype to 
each place where the property is required. Something like:

    type S is ...
    subtype Up_to_Date_S is S
       with Dynamic_Predicate => Is_Up_to_Date (Up_to_Date_S);

Then all of the operations that require up-to-date S values can have 
parameters of Up_to_Date_S; the compiler will insert a check that it is in 
fact up-to-date. (But be careful: if you use such subtypes in places where 
the object can become stale behind the scenes, Ada will not recheck the 
predicate - dynamic predicates are primarily checked when a subtype 
conversion occurs, and usually only when a subtype *change* happens.)

In either case, you have to be able to write a function which returns True 
or False as to whether an object of type S is up-to-date. (If you can't do 
that, you can't use any sort of contract for the obvious reason that a 
contract has to be able to tell if it is satisfied.)

                                   Randy.