On pragma Precondition etc.

A question about syntax.

Thanks to GNAT 2008, there is now some initial support
for stating preconditions and postconditions of supprograms,
using pragma Pre-/Postcondition.
Randy Brukardt has presented more thoughts on this to
the Ada Comments mailing list; notably, by describing
means to express a type's invariant, T'Constraint.

(GNAT's pragmas can be used to state conditions right after
the spec of a subprogram, and also at the start of
declarations of a supbrogram body. Thus,

procedure Foo(X, Y: Natural);
pragma Precondition(X > Y)

My question is about the syntactical link of a Pre-/Postcondition
to a subprogram declaration. Using GNAT's approach, the link is
implicit:
A spec Pre-/Postcondition applies to the immediately preceding
subprogram declaration and to nothing else.

At first sight it seems natural to *not* name the subprogram in
the Pre-/Postcondition pragma. You could refer the questioner
to the Department of Redundancy Department.
On the other hand, there are opportunities for code restructuring.
What happens to the Pre-/Postconditions then? I suggest the they
can get mixed up. For example, exchange the alphabetical
order of the following function declarations in a hurry,

function More(X, Y: Integer);
-- ...
pragma Precondition(X > 2 * Y);


function Less(X, Y: Integer);
-- ...
pragma Precondition(X < 2 * Y);


So I would contend the lack of a *local_name* parameter
in the pragmas Pre-/Postcondition.

The parameter could be like those of pragma No_Return or
pragma Inline, making the link to the subprogram explicit.

We would have something like

function More(X, Y: Integer);
-- ...
pragma Precondition(More, X > 2 * Y);


function Less(X, Y: Integer);
-- ...
pragma Precondition(Less, X < 2 * Y);


And now there is no doubt about the subprogram to which a
Pre-/Postcondition belongs. (A rule that a spec Pre-/Postcondition
pragma must come right after its subprogram will establish
consistency.)

(On the Ada Comments list, there seems to have been some agreement
that there should be some syntax in the future, perhaps obsoleting
this discussion...)

On Fri, 25 Jul 2008, Georg Bauhaus wrote:

> We would have something like
>
> function More(X, Y: Integer);
> -- ...
> pragma Precondition(More, X > 2 * Y);
>
>
> function Less(X, Y: Integer);
> -- ...
> pragma Precondition(Less, X < 2 * Y);
>
> And now there is no doubt about the subprogram to which a
> Pre-/Postcondition belongs. (A rule that a spec Pre-/Postcondition
> pragma must come right after its subprogram will establish
> consistency.)

This seems to break with overloading of subprogram names. I seem to recall
that
"pragma Inline(Foo)"
is asking to inlie *all* functions / procedures with the name "Foo". This
may be OK for inlining, but you definitively don't want to use the same
preconditions which happen to have the same way. Consider the following:

function More(X, Y: Integer) return Integer;
pragma Precondition(More, X > 2 * Y); --1--

function More(X, Y: Integer) return Boolean;
pragma Precondition(More, (X>0) or (Y>0)); --2--

function More(X, Y: Whatever) return Whatever; --3--

The intention is that precondition --1-- sticks to the function returning
Integer and precondition --2-- sticks to the one returning Boolean -- not
that both preconditions stick to both functions!

And neither precondition should stick to the function marked by --3--.
Depending on the type Whatever, that shouldn't even compile ...

So the syntactical link between a subprogram declaration and its
precondition cannot just depend on the subprogram name. But then, the
function name actually becomes redundant, and the current GNAT convention
appears to be the better one:

function More(X, Y: Integer) return Integer;
pragma Precondition(X > 2 * Y); --1--

function More(X, Y: Integer) return Boolean;
pragma Precondition((X>0) or (Y>0)); --2--

function More(X, Y: Whatever) return Whatever; --3--

An alternative would be to repeat the entire function declaration in the
pragma:

function More(X, Y: Integer) return Integer;
pragma Precondition(function More(X,Y: Integer) return Integer,
X > 2 * Y); --1--

Ada is always a bit verbose, which often is good for readability. But this
would throw a bit too much of redundant information at the reader.

Stefan



--
------ Stefan Lucks -- Bauhaus-University Weimar -- Germany ------
Stefan dot Lucks at uni minus weimar dot de
------ I love the taste of Cryptanalysis in the morning! ------

stefan-lu...@see-the.signature ha scritto:

> On Fri, 25 Jul 2008, Georg Bauhaus wrote:
>
> > We would have something like
> >
> > function More(X, Y: Integer);
> > -- ...
> > pragma Precondition(More, X > 2 * Y);
> >
> >
> > function Less(X, Y: Integer);
> > -- ...
> > pragma Precondition(Less, X < 2 * Y);
> >
> > And now there is no doubt about the subprogram to which a
> > Pre-/Postcondition belongs. (A rule that a spec Pre-/Postcondition
> > pragma must come right after its subprogram will establish
> > consistency.)
>
> This seems to break with overloading of subprogram names. I seem to recall
> that
> "pragma Inline(Foo)"
> is asking to inlie *all* functions / procedures with the name "Foo". This
> may be OK for inlining, but you definitively don't want to use the same
> preconditions which happen to have the same way. Consider the following:

What about _allowing_ for the name of the procedure to appear in
the pragma? The true syntactic link would be given by the pragma
position
and the procedure name would act as a "double check" to be sure that
things were not messed up. Of course this does not save you if you
permute the pragma of overloaded functions...

---

mockturtle wrote:

>
>
> stefan-lu...@see-the.signature ha scritto:
>
>> On Fri, 25 Jul 2008, Georg Bauhaus wrote:
>>
>> > We would have something like
>> >
>> > function More(X, Y: Integer);
>> > -- ...
>> > pragma Precondition(More, X > 2 * Y);
>> >
>> >
>> > function Less(X, Y: Integer);
>> > -- ...
>> > pragma Precondition(Less, X < 2 * Y);
>> >
>> > And now there is no doubt about the subprogram to which a
>> > Pre-/Postcondition belongs. (A rule that a spec Pre-/Postcondition
>> > pragma must come right after its subprogram will establish
>> > consistency.)
>>
>> This seems to break with overloading of subprogram names. I seem to recall
>> that
>> "pragma Inline(Foo)"
>> is asking to inlie *all* functions / procedures with the name "Foo". This
>> may be OK for inlining, but you definitively don't want to use the same
>> preconditions which happen to have the same way. Consider the following:
>
> What about _allowing_ for the name of the procedure to appear in
> the pragma? The true syntactic link would be given by the pragma
> position
> and the procedure name would act as a "double check" to be sure that
> things were not messed up. Of course this does not save you if you
> permute the pragma of overloaded functions...
>
> ---

Piling more suggestions: I understand the point of using pragmas by Gnat at
this stage, but if this is going to be standardized perhaps the syntax of a
declaration could be changed. For example:

function Foo (X, Y : Something) return Whatever with
Precondition (Blah) and
Postcondition (Urgh);

So now it is all a indivisible whole and the OP concern is gone.

I haven't seen Eiffel code. How do they do this?

Alex R. Mosteo schrieb:

> Piling more suggestions: I understand the point of using pragmas by Gnat at
> this stage, but if this is going to be standardized perhaps the syntax of a
> declaration could be changed. For example:
>
> function Foo (X, Y : Something) return Whatever with
> Precondition (Blah) and
> Postcondition (Urgh);
>
> So now it is all a indivisible whole and the OP concern is gone.
>
> I haven't seen Eiffel code. How do they do this?

feature Foo(X, Y : SOMETHING): WHATEVER is
-- short comment
require
Precondition_Name: Blah
do
...
ensure
Postcondition_Name: Urgh
end

The Pre-/Postcondition_Name serves a purpose similar to the
message parameter of Ada's pragmas.)

Eiffel's "contract view" of the class then hides the statements
of Foo. So you get a "spec".

feature Foo(X, Y : SOMETHING): WHATEVER is
-- short comment
require
Precondition_Name: Blah
ensure
Postcondition_Name: Urgh


In addition, Eiffel's Pre-/Postcondition have inheritance rules
for the conditions. Another spot where Ada would to be more
general.


--
Georg Bauhaus
Y A Time Drain http://www.9toX.de

stefan-lucks@see-the.signature writes:

> On Fri, 25 Jul 2008, Georg Bauhaus wrote:
>
>> We would have something like
>>
>> function More(X, Y: Integer);
>> -- ...
>> pragma Precondition(More, X > 2 * Y);
>>
>>
>> function Less(X, Y: Integer);
>> -- ...
>> pragma Precondition(Less, X < 2 * Y);
>>
>> And now there is no doubt about the subprogram to which a
>> Pre-/Postcondition belongs. (A rule that a spec Pre-/Postcondition
>> pragma must come right after its subprogram will establish
>> consistency.)
>
> This seems to break with overloading of subprogram names. I seem to recall
> that
> "pragma Inline(Foo)"
> is asking to inlie *all* functions / procedures with the name "Foo" This
> may be OK for inlining, but you definitively don't want to use the same
> preconditions which happen to have the same way.

I don't think it's OK for pragma Inline (or Convention, or any of the
others). The rules are confusing, especially the way they work with
renaming.

I think a better design would be to require every procedure to have a
unique name (plus, optionally, an overloaded name).

Syntax for pre/postconditions is a good idea, but for now it's a
GNAT-specific extension, so pragmas are better.

> An alternative would be to repeat the entire function declaration in the
> pragma:
>
> function More(X, Y: Integer) return Integer;
> pragma Precondition(function More(X,Y: Integer) return Integer,
> X > 2 * Y); --1--

That's syntactically illegal. The RM allows implementations to invent
pragmas, but does not allow them to modify the general syntax of
pragmas.

> would throw a bit too much of redundant information at the reader.

Yeah, that too.

- Bob

Georg Bauhaus a écrit :
> And now there is no doubt about the subprogram to which a
> Pre-/Postcondition belongs. (A rule that a spec Pre-/Postcondition
> pragma must come right after its subprogram will establish
> consistency.)

But then what to do for overloaded procedures?

Pascal.

--

--|------------------------------------------------------
--| Pascal Obry Team-Ada Member
--| 45, rue Gabriel Peri - 78114 Magny Les Hameaux FRANCE
--|------------------------------------------------------
--| http://www.obry.net
--| "The best way to travel is by means of imagination"
--|
--| gpg --keyserver wwwkeys.pgp.net --recv-key C1082595

Georg Bauhaus wrote:

> Alex R. Mosteo schrieb:
>
>> Piling more suggestions: I understand the point of using pragmas by Gnat at
>> this stage, but if this is going to be standardized perhaps the syntax of a
>> declaration could be changed. For example:
>>
>> function Foo (X, Y : Something) return Whatever with
>> Precondition (Blah) and
>> Postcondition (Urgh);
>>
>> So now it is all a indivisible whole and the OP concern is gone.
>>
>> I haven't seen Eiffel code. How do they do this?
>
> feature Foo(X, Y : SOMETHING): WHATEVER is
> -- short comment
> require
> Precondition_Name: Blah
> do
> ...
> ensure
> Postcondition_Name: Urgh
> end
>
> The Pre-/Postcondition_Name serves a purpose similar to the
> message parameter of Ada's pragmas.)
>
> Eiffel's "contract view" of the class then hides the statements
> of Foo. So you get a "spec".
>
> feature Foo(X, Y : SOMETHING): WHATEVER is
> -- short comment
> require
> Precondition_Name: Blah
> ensure
> Postcondition_Name: Urgh
>
>
> In addition, Eiffel's Pre-/Postcondition have inheritance rules
> for the conditions. Another spot where Ada would to be more
> general.

Very interesting, thanks!

Alex R. Mosteo schrieb:

> Piling more suggestions: I understand the point of using pragmas by Gnat at
> this stage, but if this is going to be standardized perhaps the syntax of a
> declaration could be changed. For example:
>
> function Foo (X, Y : Something) return Whatever with
> Precondition (Blah) and
> Postcondition (Urgh);

It too think a dedicated syntax would be best. However, I suggest to
take a good look at task and protected types for guidance.

Protected types already have an precondition. I know they are attached
to the body and a protected type blocks until the condition becomes true.

But the idea behind is still similar and so should be the syntax. Now
let me think:

Option 1:

using when - just like protected types.

function Foo (
Integer X,Y)
entry when
X > Y
exit when
Foo > X + Y
return
Integer;

Option 2:

using nicer English.

function Foo (
Integer X,Y)
on entry
X > Y
on exit
Foo > X + Y
return
Integer;

Both options would not need new keywords ;-)

And how about Invariants (http://en.wikipedia.org/wiki/Class_invariant)?

Martin

--
mailto://krischik@users.sourceforge.net
Ada programming at: http://ada.krischik.com

On Tue, 29 Jul 2008 13:18:37 +0200, Martin Krischik wrote:

> It too think a dedicated syntax would be best.

Agree.

> However, I suggest to
> take a good look at task and protected types for guidance.

No. Barriers are invisible implementation details. Pre-/post-conditions
describe the contract.

> Protected types already have an precondition. I know they are attached
> to the body and a protected type blocks until the condition becomes true.

Barrier expression is not a precondition (nor a post-condition, nor an
invariant).

> But the idea behind is still similar and so should be the syntax.

No, the syntax should be bound to the parameter types. Georg already
mentioned the inheritance issue. It is a very (probably the most) important
point, because contracts are subject to inheritance.

The problem with this is that the conditions are traditionally considered
in a more loose, untyped context. Their expressions involve all parameters.
In fact it means that they are bound to the anonymous type of the type of
subprogram parameters. This makes the issue of inheritance quite difficult,
especially, because inheritance on tuples of types is basically equivalent
multiple-dispatch. So...

> And how about Invariants (http://en.wikipedia.org/wiki/Class_invariant)?

Same problems. Syntax issues are inferior, IMO. But I agree, no more new
keywords, please! (:-))

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