From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!nntp-feed.chiark.greenend.org.uk!ewrotcd!reality.xs3.de!news.jacob-sparre.dk!franka.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail
From: "Randy Brukardt" <randy@rrsoftware.com>
Newsgroups: comp.lang.ada
Subject: Re: Question on type invariants
Date: Wed, 25 Jan 2017 16:06:26 -0600
Organization: JSA Research & Innovation
Message-ID: <o6b7h2$bdl$1@franka.jacob-sparre.dk>
References: <65f79e53-a468-4b77-8ee1-440c26a09371@googlegroups.com>
NNTP-Posting-Host: rrsoftware.com
X-Trace: franka.jacob-sparre.dk 1485381987 11701 24.196.82.226 (25 Jan 2017
 22:06:27 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Wed, 25 Jan 2017 22:06:27 +0000 (UTC)
X-Priority: 3
X-MSMail-Priority: Normal
X-Newsreader: Microsoft Outlook Express 6.00.2900.5931
X-RFC2646: Format=Flowed; Original
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157
Xref: news.eternal-september.org comp.lang.ada:33166
Date: 2017-01-25T16:06:26-06:00
List-Id: <comp.lang.ada>

"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.