Contracts in generic formal subprogram

Contracts in generic formal subprogram

[mockturtle]

Dear.all,
this is something that looked like a natural and nice idea to me, but the compiler disagree :-): specifying contracts in formal subprograms in generic declarations.  Actually,   RM 12.6 does not prohibit this on a syntactic level (a aspect_specification part is included), but the compiler complains.

To understand what I mean, please check the following real code toy-zed (can you hear the grammar screaming?)
-----------------------
generic
   type Ring is private;

   with function Divides (Num, Den : Ring) return Boolean;   
   with function Is_Invertible (X : Ring) return Boolean;   
   with function Inv (X : Ring) return Ring
     with
       Pre => Is_Invertible (X);
   
   with function Gcd (X, Y : Ring) return Ring
     with
       Post => Divides (X, Gcd'Result) and Divides (Y, Gcd'Result); 
package Pippo is
   -- stuff
end Pippo;
----------------------------------
The meaning I have in mind is something like

* For "Pre" aspect: who writes function Inv  can assume that X is invertible since Inv will never be called (by the package code, at least) with X not invertible.   Also Inv cannot have a stricter pre-condition.  In a sense, the package expects Inv to work correctly if and only if the pre-condition is true.

* For "Post" aspect: I expect that the result of GCD satisfies the post condition.  Post conditions for the actual subprogram can be stricter, as long as the post condition of the formal parameter is satisfied.  For example, if Ring is Integer, GCD could always return a positive value that divides both X and Y.  The fact that the result is positive does not hurt.

Should   the actual subprogram specify the same contract?  I am not sure (and I guess this could be a stumbling block for the adoption of this idea).  One could say that the actual subprogram gets a contract that is the AND of the actual subprogram and the contract specified in the generic declaration, it is up to the programmer to check that they are compatible.  I guess the compatibility could be verified by the compiler itself in simple cases, but I expect that this could not be feasible in some cases (maybe of academic interest?).

Riccardo

Re: Contracts in generic formal subprogram

[Dmitry A. Kazakov]

On 2023-04-08 09:00, mockturtle wrote:

> Should the actual subprogram specify the same contract? I am not sure (and I guess this could be a stumbling block for the adoption of this idea).

The general principle of substitutability is that the preconditions can 
be weakened, the postoconditions can be strengthened.

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

Re: Contracts in generic formal subprogram

[G.B.]

On 08.04.23 10:02, Dmitry A. Kazakov wrote:
> On 2023-04-08 09:00, mockturtle wrote:
> 
>> Should the actual subprogram specify the same contract? I am not sure (and I guess this could be a stumbling block for the adoption of this idea).
> 
> The general principle of substitutability is that the preconditions can be weakened, the postoconditions can be strengthened.

Side track: "weak" and "strong" alone sounding like a valuation to the
uninitiated, but neither technical nor precise; and the "objects" of
comparison of sets of conditions being implicit; and the ARM not
defining a technical term for these adjectives unless weak ordering
helps.

If these adjectives induce confusion, can they be avoided? E.g., by
instead mentioning the sets of Pre- and Post-conditions of those
actual/formal/overriding subprograms. I guess that super- and subset
relations will permit helpfully defining an ordering to be understood
(in general, if not in the ARM).

Re: Contracts in generic formal subprogram

[Dmitry A. Kazakov]

On 2023-04-11 07:56, G.B. wrote:
> On 08.04.23 10:02, Dmitry A. Kazakov wrote:
>> On 2023-04-08 09:00, mockturtle wrote:
>>
>>> Should the actual subprogram specify the same contract? I am not sure 
>>> (and I guess this could be a stumbling block for the adoption of this 
>>> idea).
>>
>> The general principle of substitutability is that the preconditions 
>> can be weakened, the postoconditions can be strengthened.
> 
> Side track: "weak" and "strong" alone sounding like a valuation to the
> uninitiated, but neither technical nor precise; and the "objects" of
> comparison of sets of conditions being implicit; and the ARM not
> defining a technical term for these adjectives unless weak ordering
> helps.

The formal meaning of weaker/stronger relation on predicates P and Q:

weaker   P => Q
stronger Q => P

The formal rationale is that if you have a proof

   P1 => P2 => P3

Then weakening P1 to P1' => P1 and strengthening P3 => P3' keeps it:

   P1' => P2 => P3'

--------------------------------------------------------
As for ARM.

Regarding dynamic checks all the above is irrelevant because dynamic 
checks are no contracts. Furthermore since the proper contracts include 
Constraint_Error or Storage_Error raised, do you really care how are you 
going to bomb your program while keeping proper contracts? (:-)) Sincere 
advise: forget about this mess.

For static checks a proof of implication is rather straightforward since 
we assume that all static predicates must be decidable anyway.

Of course, with generics you might run into troubles as you would have 
both proper contracts, i.e. the instantiated ones, and the generic ones 
expressed in generic terms. Instantiated contracts are easy to check, 
but what one would actually wish is checking generic contracts, which 
might turn impossible. The glimpse of the problem is what any Ada 
programmer knows: generic instantiations may fail to compile even if the 
actual parameters match...

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

Re: Contracts in generic formal subprogram

[Spiros Bousbouras]

On Tue, 11 Apr 2023 14:03:27 +0200
"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote:
> The formal meaning of weaker/stronger relation on predicates P and Q:
> 
> weaker   P => Q
> stronger Q => P
> 
> The formal rationale is that if you have a proof
> 
>    P1 => P2 => P3
> 
> Then weakening P1 to P1' => P1 and strengthening P3 => P3' keeps it:
> 
>    P1' => P2 => P3'

You have it backwards ; if  P1'  implies  P1  then  P1'  is stronger
than  P1 .

Re: Contracts in generic formal subprogram

[Spiros Bousbouras]

On Wed, 12 Apr 2023 02:18:45 -0000 (UTC)
Spiros Bousbouras <spibou@gmail.com> wrote:
> On Tue, 11 Apr 2023 14:03:27 +0200
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote:
> > The formal meaning of weaker/stronger relation on predicates P and Q:
> > 
> > weaker   P => Q
> > stronger Q => P
> > 
> > The formal rationale is that if you have a proof
> > 
> >    P1 => P2 => P3
> > 
> > Then weakening P1 to P1' => P1 and strengthening P3 => P3' keeps it:
> > 
> >    P1' => P2 => P3'
> 
> You have it backwards ; if  P1'  implies  P1  then  P1'  is stronger
> than  P1 .

Apologies ; it was me who got it backwards.

Re: Contracts in generic formal subprogram

[Niklas Holsti]

On 2023-04-12 6:37, Spiros Bousbouras wrote:
> On Wed, 12 Apr 2023 02:18:45 -0000 (UTC)
> Spiros Bousbouras <spibou@gmail.com> wrote:
>> On Tue, 11 Apr 2023 14:03:27 +0200
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote:
>>> The formal meaning of weaker/stronger relation on predicates P and Q:
>>>
>>> weaker   P => Q
>>> stronger Q => P
>>>
>>> The formal rationale is that if you have a proof
>>>
>>>     P1 => P2 => P3
>>>
>>> Then weakening P1 to P1' => P1 and strengthening P3 => P3' keeps it:
>>>
>>>     P1' => P2 => P3'
>>
>> You have it backwards ; if  P1'  implies  P1  then  P1'  is stronger
>> than  P1 .
> 
> Apologies ; it was me who got it backwards.


Speaking of logic in general, rather than Ada contracts in particular, I 
would say that you got it right, and Dmitry did not.

Suppose we have a theorem about geometrical figures F, and at first we 
can prove the theorem only if we assume (precondition) that the figure F 
is a square. Later we manage to improve the proof so that it holds also 
for rectangles. I would say, and I think mathematicians would say, that 
we /weakened/ the assumptions from "F is a square" to "F is a 
rectangle", and indeed the former (stronger) implies the latter 
(weaker), which is not as Dmitry defined "stronger".

Re: Contracts in generic formal subprogram

[G.B.]

On 12.04.23 05:37, Spiros Bousbouras wrote:
> On Wed, 12 Apr 2023 02:18:45 -0000 (UTC)
> Spiros Bousbouras <spibou@gmail.com> wrote:
>> On Tue, 11 Apr 2023 14:03:27 +0200
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote:
>>> The formal meaning of weaker/stronger relation on predicates P and Q:
>>>
>>> weaker   P => Q
>>> stronger Q => P
>>>
>>> The formal rationale is that if you have a proof
>>>
>>>     P1 => P2 => P3
>>>
>>> Then weakening P1 to P1' => P1 and strengthening P3 => P3' keeps it:
>>>
>>>     P1' => P2 => P3'
>>
>> You have it backwards ; if  P1'  implies  P1  then  P1'  is stronger
>> than  P1 .
> 
> Apologies ; it was me who got it backwards.

Thanks for pointing out the issue: When P_n or Q_m don't
mention the thing to which they "belong",
then how does just mentioning names of predicates clarify
to what end of the substitution the comparatives "weaker"
or "stronger" will apply? It's variance of meaning.

"The LSP paper" uses "weak" more generally.

OK, condition P is generally considered stronger than Q
if P implies Q, right? I.e., Q not without P.
Is there a commonly accepted definition of the words "weak"
and "strong", in mathematics perhaps, that justifies the
usual contextual _omissions_ from speech?

LSP uses "pre" and "post" for an object's value in a state.
There are phrases such as "stronger requirements that constrain".

Consider a different choice of adjectives:

   Given a primitive operation f of a type T,
   then a precondition of any overridden f of
   a type D descended from T must be sexier.

Does "sexy" carry more or less meaning than "weak" WRT assertions?

Re: Contracts in generic formal subprogram

[Ben Bacarisse]

Spiros Bousbouras <spibou@gmail.com> writes:

> On Wed, 12 Apr 2023 02:18:45 -0000 (UTC)
> Spiros Bousbouras <spibou@gmail.com> wrote:
>> On Tue, 11 Apr 2023 14:03:27 +0200
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote:
>> > The formal meaning of weaker/stronger relation on predicates P and Q:
>> > 
>> > weaker   P => Q
>> > stronger Q => P
>> > 
>> > The formal rationale is that if you have a proof
>> > 
>> >    P1 => P2 => P3
>> > 
>> > Then weakening P1 to P1' => P1 and strengthening P3 => P3' keeps it:
>> > 
>> >    P1' => P2 => P3'
>> 
>> You have it backwards ; if  P1'  implies  P1  then  P1'  is stronger
>> than  P1 .
>
> Apologies ; it was me who got it backwards.

No, you are correct.  If P1' => P1 then P1' /is/ stronger (or at least
no weaker) than P1.

Using upper and lower case to suggest stronger and weaker then if we
have a proof p |- Q, then we can also assert that P |- q for all
stronger premises P and weaker conclusions q.  Formally

  {p, P=>p, Q=>q} |- q

Or, written out using the deduction theorem, if we have p=>Q then we can
assert P=>q for any stronger P (so P=>p) and any weaker q (so Q=>q).

In Floyd-Hoare logic, this is embodied in the consequence rule:

  P=>p, {p}S{Q}, Q=>q
  -------------------
        {P}S{q}

which says that we can always strengthen a pre-condition and weaken a
post-condition.

However (if I've got the context right), in terms of substitution and/or
inheritance, Dmitry-Kazakov was correct to say that "The general
principle of substitutability is that the preconditions can be weakened,
the postoconditions can be strengthened".  It's just the definition that
was backwards.

-- 
Ben.

Re: Contracts in generic formal subprogram

[Dmitry A. Kazakov]

On 2023-04-12 04:18, Spiros Bousbouras wrote:
> On Tue, 11 Apr 2023 14:03:27 +0200
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote:
>> The formal meaning of weaker/stronger relation on predicates P and Q:
>>
>> weaker   P => Q
>> stronger Q => P
>>
>> The formal rationale is that if you have a proof
>>
>>     P1 => P2 => P3
>>
>> Then weakening P1 to P1' => P1 and strengthening P3 => P3' keeps it:
>>
>>     P1' => P2 => P3'
> 
> You have it backwards ; if  P1'  implies  P1  then  P1'  is stronger
> than  P1 .

Yes, you are right. Inclusion is an inverse of implication.

A weaker predicate is true on a set that contains the set where the 
stronger predicate is.

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

Re: Contracts in generic formal subprogram

[Randy Brukardt]

Ada 2022 allows such contracts; Ada 2012 did not. (See 6.1.1, and 
specifically 6.1.1(1/5)). Whether your compiler has caught up, who knows.

Logically the contracts should "match" (with the weakening/strengthing that 
Dmitry mentioned), but that was too hard for Ada, so they're just additive. 
(A proper matching mechanism is more the sort of thing that SPARK does, Ada 
only enforces these contracts at runtime) That is, when you call through a 
generic formal subprogram, you enforce the preconditions of both the formal 
and the actual subprogram, and similarly for the postconditions. If they 
mismatch, you might not be able to make a successful call. If it hurts, 
don't do that. ;-)

                     Randy.


"mockturtle" <framefritti@gmail.com> wrote in message 
news:0c555ce7-0b2e-49f1-8930-c4f4796793e4n@googlegroups.com...
Dear.all,
this is something that looked like a natural and nice idea to me, but the 
compiler disagree :-): specifying contracts in formal subprograms in generic 
declarations.  Actually,   RM 12.6 does not prohibit this on a syntactic 
level (a aspect_specification part is included), but the compiler complains.

To understand what I mean, please check the following real code toy-zed (can 
you hear the grammar screaming?)
-----------------------
generic
   type Ring is private;

   with function Divides (Num, Den : Ring) return Boolean;
   with function Is_Invertible (X : Ring) return Boolean;
   with function Inv (X : Ring) return Ring
     with
       Pre => Is_Invertible (X);

   with function Gcd (X, Y : Ring) return Ring
     with
       Post => Divides (X, Gcd'Result) and Divides (Y, Gcd'Result);
package Pippo is
   -- stuff
end Pippo;
----------------------------------
The meaning I have in mind is something like

* For "Pre" aspect: who writes function Inv  can assume that X is invertible 
since Inv will never be called (by the package code, at least) with X not 
invertible.   Also Inv cannot have a stricter pre-condition.  In a sense, 
the package expects Inv to work correctly if and only if the pre-condition 
is true.

* For "Post" aspect: I expect that the result of GCD satisfies the post 
condition.  Post conditions for the actual subprogram can be stricter, as 
long as the post condition of the formal parameter is satisfied.  For 
example, if Ring is Integer, GCD could always return a positive value that 
divides both X and Y.  The fact that the result is positive does not hurt.

Should   the actual subprogram specify the same contract?  I am not sure 
(and I guess this could be a stumbling block for the adoption of this idea). 
One could say that the actual subprogram gets a contract that is the AND of 
the actual subprogram and the contract specified in the generic declaration, 
it is up to the programmer to check that they are compatible.  I guess the 
compatibility could be verified by the compiler itself in simple cases, but 
I expect that this could not be feasible in some cases (maybe of academic 
interest?).

Riccardo 

Re: Contracts in generic formal subprogram

[Simon Wright]

GCC 12.2.0 accepts this code with -gnat2022.

Re: Contracts in generic formal subprogram

[mockturtle]

On Saturday, April 8, 2023 at 6:48:14 PM UTC+2, Simon Wright wrote:
> GCC 12.2.0 accepts this code with -gnat2022.

True!  Cool...  In my opinion, contracts are among the coolest (and maybe more exclusive) features of Ada