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

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

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 K 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);

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

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

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

And neither precondition should stick to the function marked by
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);

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

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

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);

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!

Dmitry A. Kazakov schrieb:

>For the Class Invariant, Randy Brukardt has mentioned
>>
>for T'Constraint use Function_Name;
>
I don't want names of conditions contaminating the program name spaces,
like generics do. Semantically they belong to a different program. This
should be syntactically visible.

The attribute 'Constraint is meant to be a language defined
attribute, just like 'Write is.

Dmitry A. Kazakov schrieb:
Tue, 29 Jul 2008 17:55:18 +0200, Georg Bauhaus wrote:

>What if one precondition states a relation between two suprogram
>parameters, or between properties of two suprogram parameters?
>
This case is equivalent to full multiple dispatch. Ada does not have it. If
it had multiple dispatch then it would clearer how to deal with the
corresponding contracts (=conditions).

How about this: For the purpose of expressing the contract
of a subprogram, dream up its "contract-type". Base this type on

(1) the precursor's contract-type (up the derivation hierarchy)
(2) the profile

So given

function Foo(X, Y: Integer) return Whatever;

denote the precondition of its "contract-type" by something like

Foo'Precondition;

Dmitry A. Kazakov schrieb:
Tue, 29 Jul 2008 17:55:18 +0200, Georg Bauhaus wrote:

>What if one precondition states a relation between two suprogram
>parameters, or between properties of two suprogram parameters?
>
This case is equivalent to full multiple dispatch. Ada does not have it. If
it had multiple dispatch then it would clearer how to deal with the
corresponding contracts (=conditions).


Design by C„¢ has been made to be a *design* tool.
It starts from the simple truth that we will likely think
about pre/post of subprograms once the language suggests we
can. The checking mechanism supports us by checking our
assumptions as good as it possibly can do this.


DbC is not meant to be reduced to a static proof tool.

Dmitry A. Kazakov schrieb:
Wed, 30 Jul 2008 11:06:16 +0200, Georg Bauhaus wrote:

>(1) the precursor's contract-type (up the derivation hierarchy)
>(2) the profile
>>
>So given
>>
>function Foo(X, Y: Integer) return Whatever;
>>
>denote the precondition of its "contract-type" by something like
>>
>Foo'Precondition;
>

>
In presence of:
>
subtype My_Integer is Integer range 1500;
type My_Whatever is new Whatever with private;
>
what are the preconditions of Foo defined on the tuples:
>
Integer x My_Integer x Whatever
My_Integer x Integer x Whatever
[some more combinations]

Any preconditions are those that you specify, of course.
They don't magically start to exist[*], and DbC adds no
magic for excluding subtle contradictions. course,
Boolean expressions involving the subprogram parameters
will be checked by the compiler. Just like with Ada; they
are checked now,

pragma Precondition(<boolean expression>);

with some rules for what can be part of <boolean expression>.
No more, no less.

Now the rules that say how preconditions are to be logically
connected when overriding. Go ahead! First,
do you want a derived object to be a suitable argument for a
parent's procedure? With or without preconditions, arguments
may meet both: the type constraints that Ada has to offer,
and the DbC constraints. Let's see,


type Whatever is tagged private;

procedure Foo(Item: Whatever);
-- pre: permissible values of Item


type My_Whatever is new Whatever with private;

overriding
procedure Foo(Item: My_Whatever);
-- pre: permissible values at least as above

X: Whatever'Class := ;
begin

Foo(X);

end;

In this case object X must satisfy the parent's preconditions
for calling Foo and the child's preconditions for calling its
Foo. So the rule would be to "weaken" the precondition in child
overridings. The phrase "at least" from the comment on the
overridden Foo translates into "or else". Theory then says,
"When overriding, only add permissible values, do not remove any."

For extended records I find this rule strikingly obvious, because
every component added to the parent type will enlarge the set of
values available in the child type.

Seen in this light, range 1 500 takes away values
from Integer'range. (Not surprisingly, since it is a constraint.)

subtype My_Integer is Integer range 1 500;

overriding
procedure Bar(Item: My_Whatever; Num: My_Integer);

With or without DbC, it seems reasonable to me to expect
that Bar fails when it gets an argument for Num outside
range 1 500. Say it fails with a Constraint_Error.

This exceptional behavior is already illustrating why the DbC
idea of having a 'Constraint on a type makes sense. It is
already working for subtypes now.

With or without DbC, you can always be troubled by the typical
variance problems, for which, as you have said before, there is
no universally good solution. Many shrug when they
are more busy with the practical benefits of DbC.



[*] Sofcheck's tools can extract a number of assertions.
There is also an Eiffel(?) tool doing similar things.
But this is beside the point when you want to design a
provable DbC component (typically, a tagged type).
It adds nothing in the sense of DbC, just more assertions
for us that help with analyzing our programs which would
typically lack assertions.

Dmitry A. Kazakov wrote:

>Any preconditions are those that you specify, of course.
>They don't magically start to exist[*],
>
course they do. If there is no explicit precondition specified for an
argument X of the type T, it still exists, and is:
>
X in T [and true]

K. They usually say "silly argument" in DbC discussions.


when you hang some contracted constraints on the
parameters of a subprogram, you implicitly define a set of derived types
constrained to that.

I could define artificial types so that Boolean expressions
could become primitive Boolean functions of that artificial type.
But I don't. What's the big gain?



[a liberal explanation of LSP skipped]
>
>Seen in this light, range 1 500 takes away values
>from Integer'range. (Not surprisingly, since it is a constraint.)
>>
>subtype My_Integer is Integer range 1 500;
>>
>overriding
>procedure Bar(Item: My_Whatever; Num: My_Integer);
>>
>With or without DbC, it seems reasonable to me to expect
>that Bar fails when it gets an argument for Num outside
>range 1 500. Say it fails with a Constraint_Error.
>
No, it fails at compile time, provided, 1 500 goes into the contract,
because the result is not LSP-conform.

An Ada compiler will compile the code,

function Foo(X: My_Integer);
pragma Precondition(X <= 500);

Bound := 501;

Foo(Bound);

My compiler may warn that the program will raise a Constraint_Error,
but the code is legal. The Precondition isn't checked
at runtime because the constraint violation happens earlier,
as this is Ada.


But the question was different. It was about composition of conditions in
presence of tuples of parameters. You consider each parameter and its
contracted constraints independently, this is wrong.

In what frame of reference is it wrong to express a boolean relation
between parameters? What is wrong with pragma Precondition?


>This exceptional behavior is already illustrating why the DbC
>idea of having a 'Constraint on a type makes sense. It is
>already working for subtypes now.
>
Wrong. Ada constraints are not contracts.

In the sense of Design by Contract Ada constraints add to a contract,
even though it is a trivial one like X in My_Integer'range.
(As I said, there might be variance problems because Ada subtypes are
superclasses considering only the set of values.
Writing Ada, you are always free to design variance problems
using 'Class parameters. I don't see a reason why Ada-DbC cannot
enhance this situation.)



>Many shrug when they
>are more busy with the practical benefits of DbC.
>
I don't buy it. Practice unsupported by a sound theory is shamanism.

DbC is about programming, in addition to being about programs.
Is there a sound theory of programming? We do have some sound
theories concerned with aspects of programs. These aspects
can be extracted from just the program. Assertion checking
in the Design(!) by Contract sense never looses sight of the process
of programming. (Neither does the word "pragma" as in
pragma Precondition.)

Could you point to your definition of "contract"? It seems to
differ from what everyone around Design by Contract understands
it to be (and understands pragma Precondition as it is now).



BTW, we could drop the idea of making conditions [<del>]contracted[</del>]
<ins>a statically verifiable property of some hypothetic type
system</ins>.

Instead of
that, we would consider constraints in the sense of Ada subtypes.

Yes?

In that case it would be [<del>]all[</del>] dynamic, run-time,
<ins>as well as food for the compiler</ins>.

[Contracted constraints are more like SPARK model] But in any case the
problem would remain. We would have to introduce anonymous subtypes
of tuples of [sub]types.

Checking a condition means calling a well defined functions at
well defined times.

In both cases we need a [sub]type to associate the
constraint with.

Why?