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!feeder.eternal-september.org!news.uzoreto.com!news.etla.org!nntp-feed.chiark.greenend.org.uk!ewrotcd!newsfeed.xs3.de!io.xs3.de!news.jacob-sparre.dk!franka.jacob-sparre.dk!pnx.dk!.POSTED.rrsoftware.com!not-for-mail
From: "Randy Brukardt" <randy@rrsoftware.com>
Newsgroups: comp.lang.ada
Subject: Re: Interesting article on ARG work
Date: Thu, 5 Apr 2018 16:23:53 -0500
Organization: JSA Research & Innovation
Message-ID: <pa645a$1lg$1@franka.jacob-sparre.dk>
References: <p9s890$mmt$1@franka.jacob-sparre.dk>
 <1b44444f-c1b3-414e-84fb-8798961487c3@googlegroups.com>
 <62ee0aac-49da-4925-b9aa-a16695b3fc45@googlegroups.com>
 <pa0vga$rbe$1@franka.jacob-sparre.dk>
 <9879872e-c18a-4667-afe5-41ce0f54559f@googlegroups.com>
 <pa3jmj$9n3$1@franka.jacob-sparre.dk> <87o9iyk2y9.fsf@nightsong.com>
 <1e3a9818-7c9a-4a8e-a6fb-ebaabd2570f7@googlegroups.com>
Injection-Date: Thu, 5 Apr 2018 21:23:54 -0000 (UTC)
Injection-Info: franka.jacob-sparre.dk;
 posting-host="rrsoftware.com:24.196.82.226";
	logging-data="1712"; mail-complaints-to="news@jacob-sparre.dk"
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.7246
Xref: reader02.eternal-september.org comp.lang.ada:51346
Date: 2018-04-05T16:23:53-05:00
List-Id: <comp.lang.ada>

"Mehdi Saada" <00120260a@gmail.com> wrote in message 
news:1e3a9818-7c9a-4a8e-a6fb-ebaabd2570f7@googlegroups.com...
...
>.. One thing I found (a bit) irritating from a beginner point of view,
> is that normal visibility rules still still holds in contracts/assertions. 
> It
> would be much easier to write contracts about conditions of (at
> least) things declared in the private part. It would be nonsensical to
> let them reach the body though, that I can understand. But why not
> packages' private part ?

A subprogram contract is just that - a contract between the caller and 
called subprogram. That means the caller needs to be able to understand the 
contents of the contract, and given that they are not supposed to depend on 
the private part, the contract can't either.

Imagine that items in the private part were allowed. Perhaps we'd have a 
contract like:

    package Something is
        type Bar is ...;
        procedure Proc (Foo : in out Bar)
           with Pre => Is_Groddy (Foo);
    private
        function Is_Groddy (Foo : in Bar) return Boolean;
    end Something;

Now,  the caller is not supposed to call Something.Proc when Is_Groddy is 
false (that's the contract). Perhaps the caller wants to make the test 
themselves (think of how often you test for null with access types before 
making a call):

     if Is_Groddy (My_Bar) then
          Proc (My_Bar);
     else
           -- Some alternative code.
     end if;

But the above is illegal, because Is_Groddy is in the private part and not 
available to the callers of Proc. This leaves the programmer with only bad 
options: make the call unconditionally and hope that My_Bar is in fact 
Groddy -- or handle the Assertion_Errror (generally more expensive than a 
test). (And if you are doing static checking, you end up depending 
explicitly on the private part, meaning you are no longer hiding it in any 
way.)

Regardless of what private information was in the contract, it is not useful 
to the caller (unless they also break privacy and inspect the private part). 
That pretty much defeats the purpose of making it private in the first 
place.

                                 Randy.