Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.

Dismiss

100 views

Skip to first unread message

Apr 8, 2023, 3:00:39 AM4/8/23

to

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

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

Apr 8, 2023, 4:02:35 AM4/8/23

to

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

be weakened, the postoconditions can be strengthened.

--

Regards,

Dmitry A. Kazakov

http://www.dmitry-kazakov.de

Apr 8, 2023, 5:09:43 AM4/8/23

to

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

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

Apr 8, 2023, 12:48:14 PM4/8/23

to

GCC 12.2.0 accepts this code with -gnat2022.

Apr 8, 2023, 1:27:17 PM4/8/23

to

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
> GCC 12.2.0 accepts this code with -gnat2022.

Apr 11, 2023, 1:56:49 AM4/11/23

to

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

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

Apr 11, 2023, 8:03:30 AM4/11/23

to

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

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

Apr 11, 2023, 10:18:49 PM4/11/23

to

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

than P1 .

Apr 11, 2023, 11:37:37 PM4/11/23

to

Apr 12, 2023, 2:49:40 AM4/12/23

to

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

Apr 12, 2023, 3:30:58 AM4/12/23

to

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?

Apr 12, 2023, 8:29:54 AM4/12/23

to

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.

Apr 13, 2023, 2:27:33 AM4/13/23

to

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

stronger predicate is.

0 new messages

Search

Clear search

Close search

Google apps

Main menu