* On pragma Precondition etc. @ 2008-07-25 8:01 Georg Bauhaus 2008-07-25 10:50 ` stefan-lucks 2008-07-25 16:50 ` Pascal Obry 0 siblings, 2 replies; 24+ messages in thread From: Georg Bauhaus @ 2008-07-25 8:01 UTC (permalink / raw) 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...) ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: On pragma Precondition etc. 2008-07-25 8:01 On pragma Precondition etc Georg Bauhaus @ 2008-07-25 10:50 ` stefan-lucks 2008-07-25 11:05 ` mockturtle 2008-07-25 14:39 ` Robert A Duff 2008-07-25 16:50 ` Pascal Obry 1 sibling, 2 replies; 24+ messages in thread From: stefan-lucks @ 2008-07-25 10:50 UTC (permalink / raw) 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! ------ ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: On pragma Precondition etc. 2008-07-25 10:50 ` stefan-lucks @ 2008-07-25 11:05 ` mockturtle 2008-07-25 11:44 ` Alex R. Mosteo 2008-07-25 14:39 ` Robert A Duff 1 sibling, 1 reply; 24+ messages in thread From: mockturtle @ 2008-07-25 11:05 UTC (permalink / raw) 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... --- ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: On pragma Precondition etc. 2008-07-25 11:05 ` mockturtle @ 2008-07-25 11:44 ` Alex R. Mosteo 2008-07-25 11:56 ` Georg Bauhaus 2008-07-29 11:18 ` Martin Krischik 0 siblings, 2 replies; 24+ messages in thread From: Alex R. Mosteo @ 2008-07-25 11:44 UTC (permalink / raw) 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? ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: On pragma Precondition etc. 2008-07-25 11:44 ` Alex R. Mosteo @ 2008-07-25 11:56 ` Georg Bauhaus 2008-07-28 8:02 ` Alex R. Mosteo 2008-07-29 11:18 ` Martin Krischik 1 sibling, 1 reply; 24+ messages in thread From: Georg Bauhaus @ 2008-07-25 11:56 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: On pragma Precondition etc. 2008-07-25 11:56 ` Georg Bauhaus @ 2008-07-28 8:02 ` Alex R. Mosteo 0 siblings, 0 replies; 24+ messages in thread From: Alex R. Mosteo @ 2008-07-28 8:02 UTC (permalink / raw) 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! ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: On pragma Precondition etc. 2008-07-25 11:44 ` Alex R. Mosteo 2008-07-25 11:56 ` Georg Bauhaus @ 2008-07-29 11:18 ` Martin Krischik 2008-07-29 12:08 ` Dmitry A. Kazakov 1 sibling, 1 reply; 24+ messages in thread From: Martin Krischik @ 2008-07-29 11:18 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: On pragma Precondition etc. 2008-07-29 11:18 ` Martin Krischik @ 2008-07-29 12:08 ` Dmitry A. Kazakov 2008-07-29 14:19 ` Georg Bauhaus 0 siblings, 1 reply; 24+ messages in thread From: Dmitry A. Kazakov @ 2008-07-29 12:08 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: On pragma Precondition etc. 2008-07-29 12:08 ` Dmitry A. Kazakov @ 2008-07-29 14:19 ` Georg Bauhaus 2008-07-29 14:49 ` Georg Bauhaus 2008-07-29 15:00 ` Dmitry A. Kazakov 0 siblings, 2 replies; 24+ messages in thread From: Georg Bauhaus @ 2008-07-29 14:19 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: On pragma Precondition etc. 2008-07-29 14:19 ` Georg Bauhaus @ 2008-07-29 14:49 ` Georg Bauhaus 2008-07-29 15:00 ` Dmitry A. Kazakov 1 sibling, 0 replies; 24+ messages in thread From: Georg Bauhaus @ 2008-07-29 14:49 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: On pragma Precondition etc. 2008-07-29 14:19 ` Georg Bauhaus 2008-07-29 14:49 ` Georg Bauhaus @ 2008-07-29 15:00 ` Dmitry A. Kazakov 2008-07-29 15:14 ` Georg Bauhaus 2008-07-29 15:55 ` Georg Bauhaus 1 sibling, 2 replies; 24+ messages in thread From: Dmitry A. Kazakov @ 2008-07-29 15:00 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: On pragma Precondition etc. 2008-07-29 15:00 ` Dmitry A. Kazakov @ 2008-07-29 15:14 ` Georg Bauhaus 2008-07-29 15:55 ` Georg Bauhaus 1 sibling, 0 replies; 24+ messages in thread From: Georg Bauhaus @ 2008-07-29 15:14 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: On pragma Precondition etc. 2008-07-29 15:00 ` Dmitry A. Kazakov 2008-07-29 15:14 ` Georg Bauhaus @ 2008-07-29 15:55 ` Georg Bauhaus 2008-07-29 17:49 ` Dmitry A. Kazakov 1 sibling, 1 reply; 24+ messages in thread From: Georg Bauhaus @ 2008-07-29 15:55 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: On pragma Precondition etc. 2008-07-29 15:55 ` Georg Bauhaus @ 2008-07-29 17:49 ` Dmitry A. Kazakov 2008-07-30 9:06 ` Georg Bauhaus 2008-07-30 9:22 ` Georg Bauhaus 0 siblings, 2 replies; 24+ messages in thread From: Dmitry A. Kazakov @ 2008-07-29 17:49 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: On pragma Precondition etc. 2008-07-29 17:49 ` Dmitry A. Kazakov @ 2008-07-30 9:06 ` Georg Bauhaus 2008-07-30 13:47 ` Dmitry A. Kazakov 2008-07-30 9:22 ` Georg Bauhaus 1 sibling, 1 reply; 24+ messages in thread From: Georg Bauhaus @ 2008-07-30 9:06 UTC (permalink / raw) 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; ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: On pragma Precondition etc. 2008-07-30 9:06 ` Georg Bauhaus @ 2008-07-30 13:47 ` Dmitry A. Kazakov 2008-07-30 17:45 ` Georg Bauhaus 0 siblings, 1 reply; 24+ messages in thread From: Dmitry A. Kazakov @ 2008-07-30 13:47 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: On pragma Precondition etc. 2008-07-30 13:47 ` Dmitry A. Kazakov @ 2008-07-30 17:45 ` Georg Bauhaus 2008-07-31 8:12 ` Dmitry A. Kazakov 0 siblings, 1 reply; 24+ messages in thread From: Georg Bauhaus @ 2008-07-30 17:45 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: On pragma Precondition etc. 2008-07-30 17:45 ` Georg Bauhaus @ 2008-07-31 8:12 ` Dmitry A. Kazakov 2008-07-31 23:06 ` Georg Bauhaus 0 siblings, 1 reply; 24+ messages in thread From: Dmitry A. Kazakov @ 2008-07-31 8:12 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: On pragma Precondition etc. 2008-07-31 8:12 ` Dmitry A. Kazakov @ 2008-07-31 23:06 ` Georg Bauhaus 2008-08-01 8:40 ` Dmitry A. Kazakov 0 siblings, 1 reply; 24+ messages in thread From: Georg Bauhaus @ 2008-07-31 23:06 UTC (permalink / raw) 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? ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: On pragma Precondition etc. 2008-07-31 23:06 ` Georg Bauhaus @ 2008-08-01 8:40 ` Dmitry A. Kazakov 0 siblings, 0 replies; 24+ messages in thread From: Dmitry A. Kazakov @ 2008-08-01 8:40 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: On pragma Precondition etc. 2008-07-29 17:49 ` Dmitry A. Kazakov 2008-07-30 9:06 ` Georg Bauhaus @ 2008-07-30 9:22 ` Georg Bauhaus 2008-07-30 13:56 ` Dmitry A. Kazakov 1 sibling, 1 reply; 24+ messages in thread From: Georg Bauhaus @ 2008-07-30 9:22 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: On pragma Precondition etc. 2008-07-30 9:22 ` Georg Bauhaus @ 2008-07-30 13:56 ` Dmitry A. Kazakov 0 siblings, 0 replies; 24+ messages in thread From: Dmitry A. Kazakov @ 2008-07-30 13:56 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: On pragma Precondition etc. 2008-07-25 10:50 ` stefan-lucks 2008-07-25 11:05 ` mockturtle @ 2008-07-25 14:39 ` Robert A Duff 1 sibling, 0 replies; 24+ messages in thread From: Robert A Duff @ 2008-07-25 14:39 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: On pragma Precondition etc. 2008-07-25 8:01 On pragma Precondition etc Georg Bauhaus 2008-07-25 10:50 ` stefan-lucks @ 2008-07-25 16:50 ` Pascal Obry 1 sibling, 0 replies; 24+ messages in thread From: Pascal Obry @ 2008-07-25 16:50 UTC (permalink / raw) To: rm.tsoh+bauhaus 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 ^ permalink raw reply [flat|nested] 24+ messages in thread
end of thread, other threads:[~2008-08-01 8:40 UTC | newest] Thread overview: 24+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2008-07-25 8:01 On pragma Precondition etc Georg Bauhaus 2008-07-25 10:50 ` stefan-lucks 2008-07-25 11:05 ` mockturtle 2008-07-25 11:44 ` Alex R. Mosteo 2008-07-25 11:56 ` Georg Bauhaus 2008-07-28 8:02 ` Alex R. Mosteo 2008-07-29 11:18 ` Martin Krischik 2008-07-29 12:08 ` Dmitry A. Kazakov 2008-07-29 14:19 ` Georg Bauhaus 2008-07-29 14:49 ` Georg Bauhaus 2008-07-29 15:00 ` Dmitry A. Kazakov 2008-07-29 15:14 ` Georg Bauhaus 2008-07-29 15:55 ` Georg Bauhaus 2008-07-29 17:49 ` Dmitry A. Kazakov 2008-07-30 9:06 ` Georg Bauhaus 2008-07-30 13:47 ` Dmitry A. Kazakov 2008-07-30 17:45 ` Georg Bauhaus 2008-07-31 8:12 ` Dmitry A. Kazakov 2008-07-31 23:06 ` Georg Bauhaus 2008-08-01 8:40 ` Dmitry A. Kazakov 2008-07-30 9:22 ` Georg Bauhaus 2008-07-30 13:56 ` Dmitry A. Kazakov 2008-07-25 14:39 ` Robert A Duff 2008-07-25 16:50 ` Pascal Obry
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox