* Assertions in the Next Ada Standard @ 2002-01-11 6:20 Richard Riehle 2002-01-11 9:23 ` Dale Stanbrough 2002-01-11 20:07 ` FGD 0 siblings, 2 replies; 16+ messages in thread From: Richard Riehle @ 2002-01-11 6:20 UTC (permalink / raw) I raised this question several months ago and it seems to have failed to catch any sustained interest. The subject came up again in a phone conversation with ARG member, Randy Brukardt. According to Randy, we need a well-crafted proposal to present to the next ARG meeting in February. I seem to recall that some people were already working on this. Has there been any progress? Will the proposal be ready for the next ARG meeting? I am willing to participate in the proposal development process, and I am sure there are others who would do so. However, I understand that someone has already started it, and there is no point in having multiple conflicting proposals. I am hoping to see something like pre-conditions, post-conditions, and invariants in the next revision of Ada. I would be pleased if we simply adopted the wording already used in Eiffel: require, ensure, and invariant, but I am not intractable about the terminology. So, who is working on the proposal for this? Richard Riehle ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Assertions in the Next Ada Standard 2002-01-11 6:20 Assertions in the Next Ada Standard Richard Riehle @ 2002-01-11 9:23 ` Dale Stanbrough 2002-01-11 13:47 ` Robert A Duff 2002-01-11 23:28 ` Nick Roberts 2002-01-11 20:07 ` FGD 1 sibling, 2 replies; 16+ messages in thread From: Dale Stanbrough @ 2002-01-11 9:23 UTC (permalink / raw) Richard Riehle wrote: > I am hoping to see something like pre-conditions, post-conditions, > and invariants in the next revision of Ada. I would be pleased if > we simply adopted the wording already used in Eiffel: require, > ensure, and invariant, but I am not intractable about the terminology. > > So, who is working on the proposal for this? > > Richard Riehle I think another valuable one would be "assume" which is an assertion that allows the compiler to invoke any code optimisation it can. Dale ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Assertions in the Next Ada Standard 2002-01-11 9:23 ` Dale Stanbrough @ 2002-01-11 13:47 ` Robert A Duff 2002-01-11 23:28 ` Nick Roberts 1 sibling, 0 replies; 16+ messages in thread From: Robert A Duff @ 2002-01-11 13:47 UTC (permalink / raw) Dale Stanbrough <dstanbro@bigpond.net.au> writes: > I think another valuable one would be "assume" which is an > assertion that allows the compiler to invoke any code > optimisation it can. I think that's equivalent to an assertion, plus a pragma Suppress on the assertion check. - Bob ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Assertions in the Next Ada Standard 2002-01-11 9:23 ` Dale Stanbrough 2002-01-11 13:47 ` Robert A Duff @ 2002-01-11 23:28 ` Nick Roberts 2002-01-12 1:30 ` Darren New 1 sibling, 1 reply; 16+ messages in thread From: Nick Roberts @ 2002-01-11 23:28 UTC (permalink / raw) "Dale Stanbrough" <dstanbro@bigpond.net.au> wrote in message news:dstanbro-07F79B.20222311012002@mec2.bigpond.net.au... > Richard Riehle wrote: > > > I am hoping to see something like pre-conditions, post-conditions, > > and invariants in the next revision of Ada. I would be pleased if > > we simply adopted the wording already used in Eiffel: require, > > ensure, and invariant, but I am not intractable about the terminology. > > > > So, who is working on the proposal for this? > > > > Richard Riehle > > I think another valuable one would be "assume" which is an > assertion that allows the compiler to invoke any code > optimisation it can. A counter-argument to the addition of any of these facilities being added can be illustrated in the following procedure: subtype Must_Be_True is Boolean range True..True; procedure P (...) is ... [invar.]: constant ... := [i. expr.]; --D [a. name]: constant Must_Be_True := [assumption]; --D begin if [debug] and then not [pre-conditions] then raise [excep.]; end if; --D ... if [debug] and then not [post-conditions] then raise [excep.]; end if; --D if [debug] and then not [invar.] /= [i. expr.] then raise [excep.]; end if; --D end P; This procedure demonstrates how pre-conditions, post-conditions, invariants, and assumptions can all be programmed in existing Ada. For efficiency, certain assumptions may be made of the compiler, in terms of static evaluation and/or dead code removal (but these would effectively be required for the efficient implementation of the proposed pragmas). A procedure such as P could be made a 'wrapper' to another Q (which does the real work). P could then be replaced by Q when debugging is completed. Alternatively, a simple text modification tool could be used to remove all lines containing "--D". It may seem like an extreme form of Blimpism to argue against the suggested pragmas, but I have found in real code that I often wanted to code quite com plicated test routines into subprograms for debugging purposes. I can't believe I'm the only one who has found this. The proposed pragmas would be of little advantage in these cases (they can only take an expression). Sometimes, what sounds like a great idea turns out not to be so brilliant when you closely look at it. And sometimes, it turns out that a bigger idea subsumes it anyway. (Read on... ;-) One little thing that (I think there is wide agreement on) would be most welcome would be a 'raise ... when ...;' statement: procedure P (...) is ... [invar.]: constant ... := [i. expr.]; --D [a. name]: constant Must_Be_True := [assumption]; --D begin raise [excep.] when [debug] and then not [pre-conditions]; --D ... raise [excep.] when [debug] and then not [post-conditions]; --D raise [excep.] when [debug] and then not [invar.] /= [i. expr.]; --D end P; However, a major new feature that I would like to see introduced at the next revision would be a provision for 'separation of concerns'. As a 'straw man', this might work something like as follows. Each declarative item which is or can contain a subprogram requires a completion in Ada 95. In the case of a subprogram, the completion (the body) is permitted to be the declaration also. My proposed facility would permit multiple completions for a subprogram (separately declared). The facility would always apply to a library unit: if the unit is a package, all the subprograms in the package would be permitted multiple completions. For example, the declaration of a library procedure P might be declared: procedure P ([parameters]); A new kind of library-level declaration would allow a set of different 'aspects' to be declared, together with a pattern for the way in which they are applied to subprograms. E.g.: procedure P ([parameters]) is separate (Debugging.Before, Main_Function, Debugging.After); This declares that P has three separate completions, named Debugging.Before, Main_Function, Debugging.After. There is also a fourth optional completion, Debugging, which is a kind of 'parent' to Debugging.Before and Debugging.After. Whenever P is called, all three declared completions will be called, in the order declared. The fourth completion, Debugging, will also be called, before those for Debugging.Before and Debugging.After. The completions would look similar to current Ada subunits: separate (Main_Function) procedure P ([parameters]) is ... begin ... end P; A completion for Debugging allows for shared declarations, and an initialisation: separate (Debugging) procedure P ([parameters]) is [invar.]: constant ... := [i. expr.]; [a. name]: constant Must_Be_True := [assumption]; begin null; end P; This body will be executed before those for Debugging.Before and Debugging.After (to provide a set of common declarations for them, and possibly an initialisation). Finally, we must separately complete the final two outstanding bodies: separate (Debugging.Before) procedure P ([parameters]) is begin raise [excep.] when [debug] and then not [pre-conditions]; end P; separate (Debugging.After) procedure P ([parameters]) is begin raise [excep.] when [debug] and then not [post-conditions]; raise [excep.] when [debug] and then not [invar.] /= [i. expr.]; end P; Things get a little more complex with packages. Here we define a pattern that applies to all the subprograms the package contains implicitly. E.g.: package My_Stuff.Utilities is procedure P (...); procedure Q (...); ... end; package My_Stuff.Utilities is separate (Debugging.Before, Main_Function, Debugging.After); There are now three bodies required to fully complete this package, one for each of the three aspects. I have also chosen to make the package a child, to illustrate naming within hierarchies. Within each of the package bodies, the completions of the given aspect of each of the package's subprograms must be given. E.g.: separate (Main_Function) package My_Stuff.Utilities body is procedure P (...) is ... begin ... -- implementation of P's main functionality end; procedure Q (...) is separate; end; I have made the completion of Q a normal subunit, to illustrate the naming scheme: separate (My_Stuff.Utilities.Main_Function) procedure Q (...) is ... end Q; There would then be: separate (Debugging) package My_Stuff.Utilities is -- any declarations common to Debugging.Before and Debugging.After begin -- any initialisation code end; separate (Debugging.Before) package My_Stuff.Utilities is procedure P (...) is begin raise [excep.] when [debug] and then not [pre-conditions]; end P; procedure Q (...) is null; end; separate (Debugging.After) package My_Stuff.Utilities is procedure P (...) is begin raise [excep.] when [debug] and then not [post-conditions]; raise [excep.] when [debug] and then not [invar.] /= [i. expr.]; end P; procedure Q (...) is null; end; I have invented a new form of null procedure, which would probably be handy. (A bit analogous to the new form of null record declaration for types.) Finally, each completion would be permitted to be a completion by renaming, as normal. In many cases, this would greatly facilitate code re-use (if the design is good). Obviously there are a lot of details to fill in on this one. But hopefully it can be seen how it solves the problem of the separation of debugging code, as well as helping to solve the problems of code separation in a much wider way. -- Best wishes, Nick Roberts ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Assertions in the Next Ada Standard 2002-01-11 23:28 ` Nick Roberts @ 2002-01-12 1:30 ` Darren New 0 siblings, 0 replies; 16+ messages in thread From: Darren New @ 2002-01-12 1:30 UTC (permalink / raw) Nick Roberts wrote: > This procedure demonstrates how pre-conditions, post-conditions, invariants, > and assumptions can all be programmed in existing Ada. Except for the inheritance rules. It's a bit more complicated than you can do with in-line code, in exactly the same way that throwing exceptions and returning error-code values are different. (Note that you also forgot to check the invariant upon entry. Except for routines that initialize limited variables. Etc.) -- Darren New San Diego, CA, USA (PST). Cryptokeys on demand. The opposite of always is sometimes. The opposite of never is sometimes. ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Assertions in the Next Ada Standard 2002-01-11 6:20 Assertions in the Next Ada Standard Richard Riehle 2002-01-11 9:23 ` Dale Stanbrough @ 2002-01-11 20:07 ` FGD 2002-01-11 20:39 ` Wes Groleau 2002-01-12 7:30 ` Richard Riehle 1 sibling, 2 replies; 16+ messages in thread From: FGD @ 2002-01-11 20:07 UTC (permalink / raw) Richard Riehle wrote: > I am hoping to see something like pre-conditions, post-conditions, > and invariants in the next revision of Ada. I would be pleased if > we simply adopted the wording already used in Eiffel: require, > ensure, and invariant, but I am not intractable about the terminology. Though I'm not familiar with Eiffel and its use of those idioms, but this sounds like an attractive proposal. However, if you allow me to play Devil's advocate, could you give a concrete example where this has significant benefits. For suprograms, this doesn't seem essential because of Ada's strong typing. It may however be very useful for loops and related constructs. But I can find *weak* replacements within Ada. For invariants, enclose loops in a block statement, e.g. declare Const_X : constant Integer := X; -- invariant X Pos_Y : Positive := Y; -- ensure Y > 0 -- invariant (Y > 0) begin loop ... end loop; end; This also allows for catching exceptions locally, or use pragma Suppress to allow optimizations. For require and ensure, enclose the loop in an inlined procedure similar to the above. These replacements are weak because Ada types cannot conveniently represent assertions such as X /= 0 or X > Y for variable X and Y. Perhaps some type improvements could do the job instead? There is one place where I can see some genuine benefits. It would be possible to specify exception conditions in declarative parts, e.g. (improvised syntax) function "/" (L, R : Integer_Type) return Integer_Type; for "/" require R /= 0; function "*" (L, R : Matrix) return Matrix; for "*" require L.Columns = R.Rows; for "*" ensure return.Rows = L.Rows; for "*" ensure return.Columns = R.Columns; Or perhaps type improvements could do the job: -- Disconnected ranges? subtype Nonzero_Integer_Type is Integer_Type range Integer_Type'First .. -1 | 1 .. Integer_Type'Last; function "/" (L : Integer_Type; R : Nonzero_Integer_Type) return Integer_Type -- Dummy discriminants? function "*" (L : Matrix(Rows => M, Columns => L); R : Matrix(Rows => L, Columns => N)) return Matrix(Rows => M, Columns => N); Perhaps I'm missing something, how does Eiffel use these? -- Frank ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Assertions in the Next Ada Standard 2002-01-11 20:07 ` FGD @ 2002-01-11 20:39 ` Wes Groleau 2002-01-12 4:56 ` Robert Dewar 2002-01-12 7:30 ` Richard Riehle 1 sibling, 1 reply; 16+ messages in thread From: Wes Groleau @ 2002-01-11 20:39 UTC (permalink / raw) > declare > Const_X : constant Integer := X; > -- invariant X > Pos_Y : Positive := Y; > -- ensure Y > 0 > -- invariant (Y > 0) > begin > loop > ... > end loop; > end; The "ensure" works, but not the "invariants." Neither of those declarations prevents an assignment to X or Y. I never saw the official proposal (if there was one) but I'd think it should be inside a subprogram: pragma Require ( condition ); pragma Invariant ( condition ); pragma Ensure ( condition ); or after a subprogram declaration: pragma Require ( subprogram, condition ); pragma Invariant ( subprogram, condition ); pragma Ensure ( subprogram, condition ); Rules of scope could be based on those of Eiffel, unless Eiffel experience has shown a need for modification. Since they're pragmas, any vendor could try them out without affecting validation. -- Wes Groleau http://freepages.rootsweb.com/~wgroleau ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Assertions in the Next Ada Standard 2002-01-11 20:39 ` Wes Groleau @ 2002-01-12 4:56 ` Robert Dewar 0 siblings, 0 replies; 16+ messages in thread From: Robert Dewar @ 2002-01-12 4:56 UTC (permalink / raw) Wes Groleau <wesgroleau@spamcop.net> wrote in message news:<3C3F4D9B.79019B90@spamcop.net>... > > declare > > Const_X : constant Integer := X; > > -- invariant X > > Pos_Y : Positive := Y; > > -- ensure Y > 0 > > -- invariant (Y > 0) > > begin > > loop > > ... > > end loop; > > end; > > The "ensure" works, but not the "invariants." Neither of those > declarations prevents an assignment to X or Y. > > I never saw the official proposal (if there was one) but > I'd think it should be inside a subprogram: > > pragma Require ( condition ); > pragma Invariant ( condition ); > pragma Ensure ( condition ); > > or after a subprogram declaration: > > pragma Require ( subprogram, condition ); > pragma Invariant ( subprogram, condition ); > pragma Ensure ( subprogram, condition ); > > Rules of scope could be based on those of Eiffel, unless Eiffel > experience has shown a need for modification. > > Since they're pragmas, any vendor could try them out without > affecting validation. Probably more realistically, someone could implement these in the FSF version of GNAT perhaps. I doubt any vendor is likely to do work in this area, I certainly have not seen any significant interest from any of our supported users in such a feature. Robert Dewar Ada Core Technologies ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Assertions in the Next Ada Standard 2002-01-11 20:07 ` FGD 2002-01-11 20:39 ` Wes Groleau @ 2002-01-12 7:30 ` Richard Riehle 2002-01-12 19:58 ` FGD ` (3 more replies) 1 sibling, 4 replies; 16+ messages in thread From: Richard Riehle @ 2002-01-12 7:30 UTC (permalink / raw) FGD wrote: > Richard Riehle wrote: > > > I am hoping to see something like pre-conditions, post-conditions, > > and invariants in the next revision of Ada. I would be pleased if > > we simply adopted the wording already used in Eiffel: require, > > ensure, and invariant, but I am not intractable about the terminology. > For suprograms, this doesn't seem essential because of Ada's strong > typing. It may however be very useful for loops and related constructs. > But I can find *weak* replacements within Ada. For invariants, enclose > loops in a block statement, e.g. I have snipped the corresponding code for sake of economy. For greatest benefit, the pre-conditions, post-conditions and invariants would be declared in the package specification. The does not preclude declaring some in subprograms, but that is not my focus, at present. Taking the invariant, first. At present, there is no construct in Ada that is package-wide or type-wide except the type declaration itself. All that one can do with a type declaration is declare a range or a set of operations. OK, one can do a little more, but that is beside the point. For a type, an invariant declaration simply adds some additional rules for that type. For example, one cannot declare a discontinous range for a numeric type, but an invariant might state that a value of that numeric type cannot ever be zero. This would be stated (asserted) in the package specfication. For other types, boolean expressions could be declared that would further constrain a type with a more rigorous invariant. I will address the problem with this a little later in this posting. Pre-conditions and post-conditions would be part of the declaration of each subprogram. Post-conditions are particularly worthwhile because there is, for access to composite type parameters, potential for side-effects that might be unknown to the client of a specification. A post-condition can guarantee there are no unchecked side-effects. Pre-conditions might be less useful given many of the controls already in place for parameter lists in subprograms. However, one might declare a pre-condition that prevents a subprogram from executing if some combination of parameters is invalid. Now to the problems. First, there is the danger that one might be able to construct a self-cancelling boolean expresssion as an assertion. We are not very sophisticated in the automated theorem proving in the world of computer science, even though there is some progress. The person who constructs an assertion might be tempted to rely on it to the exclusion of more careful inspection. Second, in an inheritance scheme, what do we do about either inheriting or overriding a assertion. This problem is non-trivial. I am not sure I have the answer, and that is why there is a need for more people thinking about this than we have so far. In a later post, one beyond this one in chronology, Dr. Dewar makes a good point. He announces that within in his customer base, there has been very little interest in this feature. Given some of the other postings I have seen so far, I am not surprised since it does not seem to be a well-understood concept within the larger Ada community. Certainly, many who frequent this forum do understand it and I would expect people such as Robert Duff to weigh in with well-reasoned criticisms. The fact that there is very little demand for assertions might be said of other seldom used and little understood features already in the language. I would like to see us engage in dialogue about this idea in terms of its intrinsic merits and and potential for harm rather than depend on the immediate demand of the day-to-day current Ada practitioner. Richard Riehle ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Assertions in the Next Ada Standard 2002-01-12 7:30 ` Richard Riehle @ 2002-01-12 19:58 ` FGD 2002-01-12 21:27 ` Ed Falis 2002-01-12 22:45 ` Darren New ` (2 subsequent siblings) 3 siblings, 1 reply; 16+ messages in thread From: FGD @ 2002-01-12 19:58 UTC (permalink / raw) Ah! I see now that your proposal is deeper than what I originally thought it was. I see also that it does addresses some very real issues of Ada. As you point out yourself, when it comes to incorporating them in the current Ada framework, invariants and pre-/post-conditions are quite different. Invariants are connected to types whereas conditions pertain to subprograms and their parameters. Consider dividing it in two related proposals to avoid opposition to one reject the other. Invariants constitute a "type improvement" as I would have said in my first reply. As such they are desirable, they provide a nice way of defining disconnected ranges and imposing constraints on type discriminants for example. Safety is an issue, but we know enough to work around it. The sublanguage of assertions should be constrained so that it cannot describe conditions which are not polytime---we know how to do that. More severe restrictions will probably be imposed, and very severe restrictions should apply if some kind of non-static assertions are to be allowed. Since the sublanguage of assertions should contain boolean variables and all propositional connectives, the problem of deciding whether or not a particular assertion is ever true is NP-complete. Thus one cannot reasonably expect compile time warnings for all such conditions. Some may object to that, but I consider this to be the programmer's problem. From my perspective, invariants have many merits. The most important is that it provides a uniform way of implementing all the type improvements I ever thought of in a uniform way. I'm still not sure about pre-/post-conditions. Right now, it seems to me that the associated complexities outnumber the benefits and I'm still curious about practical applications... -- Frank ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Assertions in the Next Ada Standard 2002-01-12 19:58 ` FGD @ 2002-01-12 21:27 ` Ed Falis 0 siblings, 0 replies; 16+ messages in thread From: Ed Falis @ 2002-01-12 21:27 UTC (permalink / raw) FGD wrote: > From my perspective, invariants have many merits. The most important is > that it provides a uniform way of implementing all the type improvements > I ever thought of in a uniform way. I'm still not sure about > pre-/post-conditions. Right now, it seems to me that the associated > complexities outnumber the benefits and I'm still curious about > practical applications... In the Eiffel model, the purpose of pre and post conditions is to establish the contract between caller and callee. The practical benefit is that if a precondition is violated, then client code is where you look to find the problem; if the postcondition is violated the service code is where you start. An additional advantage of this approach is the elimination of code in services that would check explicitly for violations of the preconditions during deployment (the usual model is to enable pre and post condition checking during development, and to disable it during deployment). - Ed ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Assertions in the Next Ada Standard 2002-01-12 7:30 ` Richard Riehle 2002-01-12 19:58 ` FGD @ 2002-01-12 22:45 ` Darren New 2002-01-14 17:20 ` Robert A Duff 2002-01-14 23:16 ` Mark Lundquist 2002-01-17 6:23 ` Richard Riehle 3 siblings, 1 reply; 16+ messages in thread From: Darren New @ 2002-01-12 22:45 UTC (permalink / raw) Richard Riehle wrote: > For a type, an invariant declaration simply adds some additional rules > for that type. For example, one cannot declare a discontinous range > for a numeric type, but an invariant might state that a value of that > numeric type cannot ever be zero. This would be stated (asserted) > in the package specfication. For other types, boolean expressions > could be declared that would further constrain a type with a more > rigorous invariant. Actually, if you wanted to follow the Eiffel model for this, the invariant would be that the values of the type have to obey the invariants unless you're running the body of a primitive operation of that type. That is, if you had something like type x is new integer; invariant x /= 0; -- Or whatever syntax procedure increment(value : in out x) is begin value := value + 1; if value = 0 then value = 1; end if; end increment; then it would be legal to call increment with a value of -1, and the first line of increment would not cause an exception. > Pre-conditions and post-conditions would be part of the declaration of > each subprogram. Post-conditions are particularly worthwhile because > there is, for access to composite type parameters, potential for > side-effects > that might be unknown to the client of a specification. A post-condition > can guarantee there are no unchecked side-effects. It's really, really difficult to rule out side-effects with post-conditions. Indeed, some of the hardest post-conditions are those of side-effects. For example, you do a Put on a file, and the postcondition is very unlikely to be able to express what that actually does in terms of future Gets. > Pre-conditions might be less useful given many of the controls already > in place for parameter lists in subprograms. However, one might declare > a pre-condition that prevents a subprogram from executing if some > combination of parameters is invalid. That's generally what they're good for, yes. Like, don't pop empty stacks, don't real closed files, and stuff like that. Most any subprogram that raises an exception specific to the package would be using preconditions instead. > Now to the problems. First, there is the danger that one might be able to > construct a self-cancelling boolean expresssion as an assertion. Not sure what a "self-cancelling" boolean expression is. You mean a tautology? Or a negation of a tautology? > We > are not very sophisticated in the automated theorem proving in the > world of computer science, even though there is some progress. Actually, "we" are. It's just a very difficult problem, with lots of NP stuff involved. > The > person who constructs an assertion might be tempted to rely on it > to the exclusion of more careful inspection. Indeed. That's part of the point of doing it, at least for preconditions. If your precondition is "don't pop an empty stack", then you don't have to implement pop to handle the case of an empty stack. This is actually a good thing. Well, not that the person won't "inspect", but that the implementation will be more straightforward. > Second, in an inheritance > scheme, what do we do about either inheriting or overriding a assertion. > This problem is non-trivial. I am not sure I have the answer, and that > is why there is a need for more people thinking about this than we have > so far. This is pretty well considered in Eiffel, actually. Indeed, the strength of Eiffel's "DbC" assertions over those of just inlining boolean checks is that they *do* get inherited in the "right way". -- Darren New San Diego, CA, USA (PST). Cryptokeys on demand. The opposite of always is sometimes. The opposite of never is sometimes. ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Assertions in the Next Ada Standard 2002-01-12 22:45 ` Darren New @ 2002-01-14 17:20 ` Robert A Duff 2002-01-14 17:42 ` Darren New 0 siblings, 1 reply; 16+ messages in thread From: Robert A Duff @ 2002-01-14 17:20 UTC (permalink / raw) Darren New <dnew@san.rr.com> writes: > > Second, in an inheritance > > scheme, what do we do about either inheriting or overriding a assertion. > > This problem is non-trivial. I am not sure I have the answer, and that > > is why there is a need for more people thinking about this than we have > > so far. > > This is pretty well considered in Eiffel, actually. Indeed, the strength > of Eiffel's "DbC" assertions over those of just inlining boolean checks > is that they *do* get inherited in the "right way". The right way for Eiffel, perhaps. But Ada makes has a distinction between class-wide and specific types, which is not present in Eiffel, so the Eiffel rules don't quite translate over to Ada. I think you really want *two* preconditions on a dispatching procedure: one that applies to non-dispatching calls, and one that applies to dispatching calls. This is so the specific type can provide a stronger contract than is provided by the whole class. Same for post-cond. The Eiffel rules are certainly a good starting point. But it would require some thought to translate them into the Ada world. - Bob ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Assertions in the Next Ada Standard 2002-01-14 17:20 ` Robert A Duff @ 2002-01-14 17:42 ` Darren New 0 siblings, 0 replies; 16+ messages in thread From: Darren New @ 2002-01-14 17:42 UTC (permalink / raw) Robert A Duff wrote: > The Eiffel rules are certainly a good starting point. But it would > require some thought to translate them into the Ada world. No question. My point was that DbC *should* be more than what you could do with just a macro preprocessor translator into inline asserts. The right answer for Ada, with tasks, protected types, tagged types, limited types, etc is likely to be far more complex than for a language as simple as Eiffel. Unfortunately, I don't have enough experience with Ada to have a good idea of all the pitfalls I'd run into if I tried to work something out myself. :-) -- Darren New San Diego, CA, USA (PST). Cryptokeys on demand. The opposite of always is sometimes. The opposite of never is sometimes. ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Assertions in the Next Ada Standard 2002-01-12 7:30 ` Richard Riehle 2002-01-12 19:58 ` FGD 2002-01-12 22:45 ` Darren New @ 2002-01-14 23:16 ` Mark Lundquist 2002-01-17 6:23 ` Richard Riehle 3 siblings, 0 replies; 16+ messages in thread From: Mark Lundquist @ 2002-01-14 23:16 UTC (permalink / raw) "Richard Riehle" <richard@adaworks.com> wrote in message news:3C3FE630.BDB27416@adaworks.com... <[..snip..] > The fact that there is very little demand for assertions might be said > of other seldom used and little understood features already in the language. Good point. > > I would like to see us engage in dialogue about this idea in terms of > its intrinsic merits and and potential for harm rather than depend on the > immediate demand of the day-to-day current Ada practitioner. ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Assertions in the Next Ada Standard 2002-01-12 7:30 ` Richard Riehle ` (2 preceding siblings ...) 2002-01-14 23:16 ` Mark Lundquist @ 2002-01-17 6:23 ` Richard Riehle 3 siblings, 0 replies; 16+ messages in thread From: Richard Riehle @ 2002-01-17 6:23 UTC (permalink / raw) I appreciate the thoughtful contributions regarding assertions in next Ada standard. It was my understanding someone was drafting a proposal for this and I was hoping to see some comment from whoever that might be. Meanwhile, I clipped the following from a discussion about the assertion mechanism in Java from a discussion on comp.object. ------------------ quote from comp.object ------------------------- The documentation at Sun recommends NOT using assertions to check argument values on public methods. You should still continue to do this kind of thing with if statement and throw IllegalArgumentException. --------------------<quote from Sun>--------------------- 3.Why not provide a full-fledged design-by-contract facility with preconditions, postconditions and class invariants, like the one in the Eiffel programming language? We considered providing such a facility, but were unable to convince ourselves that it is possible to graft it onto the Java programming language without massive changes to the Java platform libraries, and massive inconsistencies between old and new libraries. Further, we were not convinced that such a facility would preserve the simplicity that is Java's hallmark. On balance, we came to the conclusion that a simple boolean assertion facility was a fairly straight-forward solution and far less risky. It's worth noting that adding a boolean assertion facility to the language doesn't preclude adding a full-fledged design- by-contract facility at some time in the future. -----------------<end of quote from Sun>------------------- ----------------- end of quote from comp.object --------------- > Richard Riehle ^ permalink raw reply [flat|nested] 16+ messages in thread
end of thread, other threads:[~2002-01-17 6:23 UTC | newest] Thread overview: 16+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2002-01-11 6:20 Assertions in the Next Ada Standard Richard Riehle 2002-01-11 9:23 ` Dale Stanbrough 2002-01-11 13:47 ` Robert A Duff 2002-01-11 23:28 ` Nick Roberts 2002-01-12 1:30 ` Darren New 2002-01-11 20:07 ` FGD 2002-01-11 20:39 ` Wes Groleau 2002-01-12 4:56 ` Robert Dewar 2002-01-12 7:30 ` Richard Riehle 2002-01-12 19:58 ` FGD 2002-01-12 21:27 ` Ed Falis 2002-01-12 22:45 ` Darren New 2002-01-14 17:20 ` Robert A Duff 2002-01-14 17:42 ` Darren New 2002-01-14 23:16 ` Mark Lundquist 2002-01-17 6:23 ` Richard Riehle
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox