On pragma Precondition etc.

On pragma Precondition etc.

[Georg Bauhaus]

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

Re: On pragma Precondition etc.

[stefan-lucks]

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

Re: On pragma Precondition etc.

[mockturtle]

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

---

Re: On pragma Precondition etc.

[Alex R. Mosteo]

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?

Re: On pragma Precondition etc.

[Georg Bauhaus]

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

Re: On pragma Precondition etc.

[Robert A Duff]

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

Re: On pragma Precondition etc.

[Pascal Obry]

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

Re: On pragma Precondition etc.

[Alex R. Mosteo]

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!

Re: On pragma Precondition etc.

[Martin Krischik]

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

Re: On pragma Precondition etc.

[Dmitry A. Kazakov]

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

Re: On pragma Precondition etc.

[Georg Bauhaus]

Dmitry A. Kazakov schrieb:
> On Tue, 29 Jul 2008 13:18:37 +0200, Martin Krischik wrote:
> 
>> It too think a dedicated syntax would be best.
>  Syntax issues are inferior, IMO. But I agree, no more new
> keywords, please! (:-))

On the other hand, overloading keywords is an invitation
to make things more puzzling. One reason is that context
is needed for disambiguation of the meaning of a keyword.


Another thing is, should conditions have parts? Possibly
named parts?  In Eiffel, multiple preconditions are
connected by "and", thus

   feature foo(X, Y: INTEGER) WHATEVER is

      Must_Have_This: X > Y
      Positive_Y:     Y > 0
      Even_X:         X rem 2 = 0

   do
      ...

The names do not add anything. However, when one of the pre-s
is false, the name is seen in the trace, and in the corresponding
EXCEPTION object.

For the Class Invariant, Randy Brukardt has mentioned

    for T'Constraint use Function_Name;


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

Re: On pragma Precondition etc.

[Georg Bauhaus]

Georg Bauhaus schrieb:

> For the Class Invariant, Randy Brukardt has mentioned
> 
>    for T'Constraint use Function_Name;
> 

Hmmm...  There is Foo'Result, already, in GNAT's "experimental"
edition. So,


    function Foo(X, Y: Integer) return Whatever;
    --  The bar of (x, y)

    for Foo'Precondition use X > Y;

Or,

    for Foo'Precondition use
       local_name => expression {, local_name => expression} ;


Or, reusing Assert and exception mechnisms

    for Foo'Precondition use
       expression with "message"
      {, expression with "another message"} ;


Should we be wanting parentheses around the aggregates of
boolean expressions?  :)


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

Re: On pragma Precondition etc.

[Dmitry A. Kazakov]

On Tue, 29 Jul 2008 16:19:20 +0200, Georg Bauhaus wrote:

> On the other hand, overloading keywords is an invitation
> to make things more puzzling.

I don't see it that way, especially after Unicode identifiers were allowed.
You can legally use *any* reserved keyword as an identifier. Just replace
vowels 'o', 'a', 'i' with their Cyrillic equivalents and enjoy.

> One reason is that context
> is needed for disambiguation of the meaning of a keyword.

So what? 

> Another thing is, should conditions have parts? Possibly
> named parts?

No, I think that any condition shall be related to a [sub]type, which gives
the name of. I prefer named equivalence.

> The names do not add anything. However, when one of the pre-s
> is false, the name is seen in the trace, and in the corresponding
> EXCEPTION object.

Conditions shall not propagate exceptions in the same partition.
 
> 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.

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

Re: On pragma Precondition etc.

[Georg Bauhaus]

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.

Re: On pragma Precondition etc.

[Georg Bauhaus]

Dmitry A. Kazakov schrieb:

>> Another thing is, should conditions have parts? Possibly
>> named parts?
> 
> No, I think that any condition shall be related to a [sub]type, which gives
> the name of. I prefer named equivalence.

What if one precondition states a relation between two suprogram
parameters, or between properties of two suprogram parameters?



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

Re: On pragma Precondition etc.

[Dmitry A. Kazakov]

On Tue, 29 Jul 2008 17:55:18 +0200, Georg Bauhaus wrote:

> Dmitry A. Kazakov schrieb:
> 
>>> Another thing is, should conditions have parts? Possibly
>>> named parts?
>> 
>> No, I think that any condition shall be related to a [sub]type, which gives
>> the name of. I prefer named equivalence.
> 
> 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).

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

Re: On pragma Precondition etc.

[Georg Bauhaus]

Dmitry A. Kazakov schrieb:
> On 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;

Re: On pragma Precondition etc.

[Georg Bauhaus]

Dmitry A. Kazakov schrieb:
> On 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 Contract™ 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.

Re: On pragma Precondition etc.

[Dmitry A. Kazakov]

On Wed, 30 Jul 2008 11:06:16 +0200, Georg Bauhaus wrote:

> Dmitry A. Kazakov schrieb:
>> On 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".

This type is obviously a tuple of the parameters of Foo.

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

Naming does not solve the problem.

In presence of:

   subtype My_Integer is Integer range 1..500;
   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
Integer x My_Integer x Whatever
My_Integer x My_Integer x Whatever
Integer x My_Integer x My_Whatever
My_Integer x Integer x My_Whatever
Integer x My_Integer x My_Whatever
My_Integer x My_Integer x My_Whatever

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

Re: On pragma Precondition etc.

[Dmitry A. Kazakov]

On Wed, 30 Jul 2008 11:22:38 +0200, Georg Bauhaus wrote:

> Dmitry A. Kazakov schrieb:
>> On 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 Contract™ has been made to be a *design* tool.

This applies to everything.

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

OK, that is another discussion.

No, correctness is a property of a given program. As such it is static per
the definition of <=> correctness of P may not depend on any of the
run-time states of P <=> P cannot be correct in one of its states and
incorrect in another <=> a correct P traverses only the states where P is
correct, etc.

Contracts *when* thought as statements about the correctness are static. I
don't care about the meaning of DbC™ as a registered trademark. I care
about Ada. (:-)) 

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

Re: On pragma Precondition etc.

[Georg Bauhaus]

Dmitry A. Kazakov schrieb:
> On 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 1..500;
>    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. Of 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.

Re: On pragma Precondition etc.

[Dmitry A. Kazakov]

On Wed, 30 Jul 2008 19:45:03 +0200, Georg Bauhaus wrote:

> Dmitry A. Kazakov schrieb:
>> On 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 1..500;
>>    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[*],

Of 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]

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

Yep, substitutability is it all about.

> With or without preconditions, arguments
> may meet both: the type constraints that Ada has to offer,
> and the DbC constraints.

The point is that when you hang some contracted constraints on the
parameters of a subprogram, you implicitly define a set of derived types
constrained to that. The subprogram become a primitive operation of these
derived types.

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

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.

> 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. A constrained subtype when it
inherits primitive operations of the unconstrained base type, also does the
contracts of these operations in full. To be LSP-conform these contracts
shall include Constraint_Error. Otherwise, that would violate
substitutability.

Ada assumes Constraint_Error in all contracts, which is quite unfortunate
for static analysis. But it was necessary to do because its exceptions are
not contracted.

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

------
BTW, we could drop the idea of making conditions contracted. Instead of
that, we would consider constraints in the sense of Ada subtypes. Which is
the model used in Eiffel. In that case it would be all dynamic, run-time.
[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. In both cases we need a [sub]type to associate the
constraint with. We cannot do it for a subprogram, except the case when it
has only one parameter.

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

Re: On pragma Precondition etc.

[Georg Bauhaus]

Dmitry A. Kazakov wrote:

>> Any preconditions are those that you specify, of course.
>> They don't magically start to exist[*],
> 
> Of 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]

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

Re: On pragma Precondition etc.

[Dmitry A. Kazakov]

On Fri, 01 Aug 2008 01:06:42 +0200, Georg Bauhaus wrote:

> Dmitry A. Kazakov wrote:
> 
>> 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?

To have it typed. When you just sow arbitrary conditions here and there,
you cannot reuse or reason about them generally. It is uninteresting and
there is pragma Assert for that. (possibility #1)

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

See, it is not a contract. If it were a contract you would not be able to
pass Bound to Foo due to a contract violation. pragma Precondition did not
change the contract of Foo.

>> 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 the semantics of the relation? #1?

> What is wrong with pragma Precondition?

1. Untyped, not reusable, cannot handle polymorphism, non-composable (and
other more or less equivalent statements)

2. Changes the program semantics (in general case cannot be ignored, and
undecidable if it could be)

3. Statically uncheckable

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

No, it adds nothing. When you create an Ada subtype the contract of the
result is not changed. It is still "X in T, and Constraint_Error may be
propagated."

> (As I said, there might be variance problems because Ada subtypes are
> superclasses considering only the set of values.

Hmm, I don't know what you mean under "superclasse" in this context.

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

I don't get the point. Is it that assertions and preconditions are merely
comments for a well-disposed reader?

Under "sound theory" I understand at least a comprehensible definition of
the semantics of conditions. Is

   pragma Precondition (X);

intended to be an abbreviation for horribly long:

   if not X then
      raise Assert_Error;
   end if;

That's one possible interpretation (#1). I don't think people would enjoy
it much. But it is still better than vague references to "practical
benefits." If you want to move beyond #1 you will face problems.

> Could you point to your definition of "contract"?

A restriction put on multiple parties (like callee/caller) identically true
in a correct program.

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

Sure (I read "hypothetic" as "strongly typed")

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

Yes. It would allow interesting so things. For example, one could define
subtypes of odd numbers, integers without zero, dimensioned values, etc.

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

Rather useless food. The compiler may not reject the program because
constraints would not influence the program semantics. [Unless exceptions
would become contracted.]

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

Because there is no other vehicle. Constraints are put on subtypes. If you
want to put constraints on sets of, which is implied by mixing multiple
parameters in one expression, then you need subtypes of tuples of types.

Of course, if you don't consider it as #1 above.

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