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
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!news4.google.com!feeder1-2.proxad.net!proxad.net!feeder1-1.proxad.net!club-internet.fr!feedme-small.clubint.net!news.ecp.fr!news.jacob-sparre.dk!pnx.dk!not-for-mail
From: "Randy Brukardt" <randy@rrsoftware.com>
Newsgroups: comp.lang.ada
Subject: Re: On pragma Precondition and types
Date: Thu, 2 Oct 2008 18:09:57 -0500
Organization: Jacob's private Usenet server
Message-ID: <gc3mem$28b$1@jacob-sparre.dk>
References: <48e4dc3b$0$6604$9b4e6d93@newsspool3.arcor-online.net>
NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net
X-Trace: jacob-sparre.dk 1222991126 2315 69.95.181.76 (2 Oct 2008 23:45:26
 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Thu, 2 Oct 2008 23:45:26 +0000 (UTC)
X-Priority: 3
X-MSMail-Priority: Normal
X-Newsreader: Microsoft Outlook Express 6.00.2900.5512
X-RFC2646: Format=Flowed; Original
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.5579
Xref: g2news2.google.com comp.lang.ada:7930
Date: 2008-10-02T18:09:57-05:00
List-Id: <comp.lang.ada>

"Georg Bauhaus" <rm.dash-bauhaus@futureapps.de> wrote in message 
news:48e4dc3b$0$6604$9b4e6d93@newsspool3.arcor-online.net...
...
> I want to add a precondition of P. The precondition
> involves F,
>
>   procedure P (X: in out T);
>   pragma Precondition (F(X));
>
>   function  F (X: T) return Boolean;
>
>
> But when the compiler sees the pragma Precondition,
> it has not yet seen F.  Therefore, by the principle
> of linear reading, the precondition cannot be compiled,
> IIUC.

You declare F first, of course. It's precondition (if any) can't depend on 
P, so there is no ordering problem. (And the order of the bodies is not 
constrained by the order of the specs.)

I suppose you could claim that F is only intended to be used in 
Preconditions and thus should be hidden somehow. But I find that dubious - 
how is the programmer going to avoid triggering the precondition if they 
can't call F to check?

For instance, in Claw, one could imagine F = Is_Valid and P = Move. It's not 
at all unusual to see code like:

    if Is_Valid (Some_Window) then
          Move (Some_Window, ...);
    end if;

Of course, if you can guarentee the precondition some other way, that's 
preferred. But it's unlikely to be the general case.

Similarly, hiding the routines in the precondition is likely to make it 
harder to understand. And a contract that is hard to understand does no one 
any favors.

So, I don't think that there will be much interest in this idea. (Not to 
mention the shreek that Adam mentioned...)

                                   Randy.