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

[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

[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" <frame...@gmail.com> wrote in message
news:0c555ce7-0b2e-49f1...@googlegroups.com...

[Simon Wright]

GCC 12.2.0 accepts this code with -gnat2022.

[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

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

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

[Spiros Bousbouras]

On Tue, 11 Apr 2023 14:03:27 +0200
"Dmitry A. Kazakov" <mai...@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 .

[Spiros Bousbouras]

Apologies ; it was me who got it backwards.

[Niklas Holsti]

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

[G.B.]

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?

[Ben Bacarisse]

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.

[Dmitry A. Kazakov]

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.