On pragma Precondition and types

On pragma Precondition and types

[Georg Bauhaus]

Suppose there is a type T with operations P and F,

   type T is private;

   procedure P (X: in out T);
   function  F (X: T) return Boolean;


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.

Could there be a rule for pragmas, say, allowing forward
references? Or can these rules be tied to some suitable
constraint syntax?

Re: On pragma Precondition and types

[Adam Beneschan]

On Oct 2, 7:35 am, Georg Bauhaus <rm.dash-bauh...@futureapps.de>
wrote:
> Suppose there is a type T with operations P and F,
>
>    type T is private;
>
>    procedure P (X: in out T);
>    function  F (X: T) return Boolean;
>
> 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.
>
> Could there be a rule for pragmas, say, allowing forward
> references?

If you just heard a strange high-pitched noise, it was the sound of
several dozen compiler maintainers reacting to your proposal in
terror.  Sort of the same sound Janet Leigh made in "Psycho"........

                                 -- Adam

Re: On pragma Precondition and types

[Randy Brukardt]

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

Re: On pragma Precondition and types

[Randy Brukardt]

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

Re: On pragma Precondition and types

[Randy Brukardt]

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

Re: On pragma Precondition and types

[Dmitry A. Kazakov]

On Thu, 2 Oct 2008 18:09:57 -0500, Randy Brukardt wrote:

> 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?

There is more in that. Preconditions semantically do not belong to the
program. Thus it makes a lot of sense to have F declared and implemented
outside it. If programs could be written in 3D space, the declaration of F
should be written orthogonal to other text... (:-))

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: On pragma Precondition and types

[Georg Bauhaus]

Dmitry A. Kazakov wrote:
> On Thu, 2 Oct 2008 18:09:57 -0500, Randy Brukardt wrote:
> 
>> 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?
> 
> There is more in that. Preconditions semantically do not belong to the
> program.

I guess that Assertion_Policy helps restoring the bug-free,
assertion-less, genuine, trouble-free, original program.

IMHO, preconditions belong to any program that is honest
about real-life programming practices. ("Our programs do
include checks affecting its operation just like anything
in it.")

Re: On pragma Precondition and types

[Dmitry A. Kazakov]

On Fri, 03 Oct 2008 11:35:45 +0200, Georg Bauhaus wrote:

> IMHO, preconditions belong to any program that is honest
> about real-life programming practices.

likewise the color of paper it is printed on...

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: On pragma Precondition and types

[Georg Bauhaus]

Dmitry A. Kazakov wrote:
> On Fri, 03 Oct 2008 11:35:45 +0200, Georg Bauhaus wrote:
> 
>> IMHO, preconditions belong to any program that is honest
>> about real-life programming practices.
> 
> likewise the color of paper it is printed on...

Right, black ink does not work well on black paper.