Re: On pragma Precondition and types

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

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