*Contracts in generic formal subprogram@ 2023-04-08 7:00 mockturtle2023-04-08 8:02 ` Dmitry A. Kazakov ` (2 more replies) 0 siblings, 3 replies; 13+ messages in thread From: mockturtle @ 2023-04-08 7:00 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 13+ messages in thread

*Re: Contracts in generic formal subprogram2023-04-08 7:00 Contracts in generic formal subprogram mockturtle@ 2023-04-08 8:02 ` Dmitry A. Kazakov2023-04-11 5:56 ` G.B. 2023-04-08 9:09 ` Randy Brukardt 2023-04-08 16:48 ` Simon Wright 2 siblings, 1 reply; 13+ messages in thread From: Dmitry A. Kazakov @ 2023-04-08 8:02 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 13+ messages in thread

*Re: Contracts in generic formal subprogram2023-04-08 7:00 Contracts in generic formal subprogram mockturtle 2023-04-08 8:02 ` Dmitry A. Kazakov@ 2023-04-08 9:09 ` Randy Brukardt2023-04-08 16:48 ` Simon Wright 2 siblings, 0 replies; 13+ messages in thread From: Randy Brukardt @ 2023-04-08 9:09 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 13+ messages in thread

*Re: Contracts in generic formal subprogram2023-04-08 7:00 Contracts in generic formal subprogram mockturtle 2023-04-08 8:02 ` Dmitry A. Kazakov 2023-04-08 9:09 ` Randy Brukardt@ 2023-04-08 16:48 ` Simon Wright2023-04-08 17:27 ` mockturtle 2 siblings, 1 reply; 13+ messages in thread From: Simon Wright @ 2023-04-08 16:48 UTC (permalink / raw) GCC 12.2.0 accepts this code with -gnat2022. ^ permalink raw reply [flat|nested] 13+ messages in thread

*2023-04-08 16:48 ` Simon WrightRe: Contracts in generic formal subprogram@ 2023-04-08 17:27 ` mockturtle0 siblings, 0 replies; 13+ messages in thread From: mockturtle @ 2023-04-08 17:27 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 13+ messages in thread

*Re: Contracts in generic formal subprogram2023-04-08 8:02 ` Dmitry A. Kazakov@ 2023-04-11 5:56 ` G.B.2023-04-11 12:03 ` Dmitry A. Kazakov 0 siblings, 1 reply; 13+ messages in thread From: G.B. @ 2023-04-11 5:56 UTC (permalink / raw) 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). ^ permalink raw reply [flat|nested] 13+ messages in thread

*Re: Contracts in generic formal subprogram2023-04-11 5:56 ` G.B.@ 2023-04-11 12:03 ` Dmitry A. Kazakov2023-04-12 2:18 ` Spiros Bousbouras 0 siblings, 1 reply; 13+ messages in thread From: Dmitry A. Kazakov @ 2023-04-11 12:03 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 13+ messages in thread

*Re: Contracts in generic formal subprogram2023-04-11 12:03 ` Dmitry A. Kazakov@ 2023-04-12 2:18 ` Spiros Bousbouras2023-04-12 3:37 ` Spiros Bousbouras 2023-04-13 6:27 ` Dmitry A. Kazakov 0 siblings, 2 replies; 13+ messages in thread From: Spiros Bousbouras @ 2023-04-12 2:18 UTC (permalink / raw) 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 . ^ permalink raw reply [flat|nested] 13+ messages in thread

*Re: Contracts in generic formal subprogram2023-04-12 2:18 ` Spiros Bousbouras@ 2023-04-12 3:37 ` Spiros Bousbouras2023-04-12 6:49 ` Niklas Holsti ` (2 more replies) 2023-04-13 6:27 ` Dmitry A. Kazakov 1 sibling, 3 replies; 13+ messages in thread From: Spiros Bousbouras @ 2023-04-12 3:37 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 13+ messages in thread

*Re: Contracts in generic formal subprogram2023-04-12 3:37 ` Spiros Bousbouras@ 2023-04-12 6:49 ` Niklas Holsti2023-04-12 7:30 ` G.B. 2023-04-12 12:29 ` Ben Bacarisse 2 siblings, 0 replies; 13+ messages in thread From: Niklas Holsti @ 2023-04-12 6:49 UTC (permalink / raw) 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". ^ permalink raw reply [flat|nested] 13+ messages in thread

*Re: Contracts in generic formal subprogram2023-04-12 3:37 ` Spiros Bousbouras 2023-04-12 6:49 ` Niklas Holsti@ 2023-04-12 7:30 ` G.B.2023-04-12 12:29 ` Ben Bacarisse 2 siblings, 0 replies; 13+ messages in thread From: G.B. @ 2023-04-12 7:30 UTC (permalink / raw) 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? ^ permalink raw reply [flat|nested] 13+ messages in thread

*Re: Contracts in generic formal subprogram2023-04-12 3:37 ` Spiros Bousbouras 2023-04-12 6:49 ` Niklas Holsti 2023-04-12 7:30 ` G.B.@ 2023-04-12 12:29 ` Ben Bacarisse2 siblings, 0 replies; 13+ messages in thread From: Ben Bacarisse @ 2023-04-12 12:29 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 13+ messages in thread

*Re: Contracts in generic formal subprogram2023-04-12 2:18 ` Spiros Bousbouras 2023-04-12 3:37 ` Spiros Bousbouras@ 2023-04-13 6:27 ` Dmitry A. Kazakov1 sibling, 0 replies; 13+ messages in thread From: Dmitry A. Kazakov @ 2023-04-13 6:27 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 13+ messages in thread

end of thread, other threads:[~2023-04-13 6:27 UTC | newest]Thread overview:13+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2023-04-08 7:00 Contracts in generic formal subprogram mockturtle 2023-04-08 8:02 ` Dmitry A. Kazakov 2023-04-11 5:56 ` G.B. 2023-04-11 12:03 ` Dmitry A. Kazakov 2023-04-12 2:18 ` Spiros Bousbouras 2023-04-12 3:37 ` Spiros Bousbouras 2023-04-12 6:49 ` Niklas Holsti 2023-04-12 7:30 ` G.B. 2023-04-12 12:29 ` Ben Bacarisse 2023-04-13 6:27 ` Dmitry A. Kazakov 2023-04-08 9:09 ` Randy Brukardt 2023-04-08 16:48 ` Simon Wright 2023-04-08 17:27 ` mockturtle

This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox