* Assertions @ 1999-05-10 0:00 J & A Richardson 1999-05-10 0:00 ` Assertions Marin David Condic 1999-05-12 0:00 ` Assertions Peter Amey 0 siblings, 2 replies; 35+ messages in thread From: J & A Richardson @ 1999-05-10 0:00 UTC (permalink / raw) I have looked through the RM and can not find any refference to assertions, pre conditions, or post conditions. It was my understanding that Ada 95 used assertions. I have also looked through a couple of webpages. Does Ada 95 use exceptions to work as assertions? Or am I missing something? Please help. James ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-10 0:00 Assertions J & A Richardson @ 1999-05-10 0:00 ` Marin David Condic 1999-05-11 0:00 ` Assertions Robert Dewar 1999-05-12 0:00 ` Assertions Peter Amey 1 sibling, 1 reply; 35+ messages in thread From: Marin David Condic @ 1999-05-10 0:00 UTC (permalink / raw) J & A Richardson wrote: > > I have looked through the RM and can not find any refference to > assertions, pre conditions, or post conditions. > > It was my understanding that Ada 95 used assertions. > > I have also looked through a couple of webpages. > > Does Ada 95 use exceptions to work as assertions? Or am I missing > something? > That depends on exactly what will count as an "assertion". If parameters to a procedure are of data types that have meaningful constraints (ranges for which the subprogram is valid) then this counts as a kind of primitive assertion. Violation of the assertion will raise an exception. But I don't think that is what you mean. The sort of assertions that would allow you to check for, say, relationships between parameters as well as valid ranges, etc., are not a standard part of Ada. However, the GNAT compiler for Ada95 has the pragma Assert which allows you to include logical expressions which can be turned on and off with compiler directives. This lets you accomplish the same thing as a direct language feature in creating preconditions, postconditions, etc. I won't swear to it, but I think the "pragma Assert" got enough attention that other compiler vendors have implemented it as well, so it is becoming a common - if not standard - feature of the language. I'd expect to see it in some future revision of the ARM. MDC -- Marin David Condic Real Time & Embedded Systems, Propulsion Systems Analysis United Technologies, Pratt & Whitney, Large Military Engines M/S 731-95, P.O.B. 109600, West Palm Beach, FL, 33410-9600 ***To reply, remove "bogon" from the domain name.*** Visit my web page at: http://www.flipag.net/mcondic ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-10 0:00 ` Assertions Marin David Condic @ 1999-05-11 0:00 ` Robert Dewar 1999-05-11 0:00 ` Assertions Nick Roberts 1999-05-12 0:00 ` Assertions Tucker Taft 0 siblings, 2 replies; 35+ messages in thread From: Robert Dewar @ 1999-05-11 0:00 UTC (permalink / raw) In article <3736F549.E3DDCDEB@pwfl.com>, diespammer@pwfl.com wrote: >but I think the "pragma Assert" got enough attention that other > compiler vendors have implemented it as well, so it is > becoming a common > - if not standard - feature of the language. I'd expect to see > it in some future revision of the ARM. I would not! I do not see that the fundamental problems that caused Assert not to make it into the Ada 95 RM have been solved. For a discussion of these problems, consult the archives (we have had that thread at least once, probably more than once in recent memory). --== Sent via Deja.com http://www.deja.com/ ==-- ---Share what you know. Learn what you don't.--- ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-11 0:00 ` Assertions Robert Dewar @ 1999-05-11 0:00 ` Nick Roberts 1999-05-11 0:00 ` Assertions Robert Dewar 1999-05-12 0:00 ` Assertions Tucker Taft 1 sibling, 1 reply; 35+ messages in thread From: Nick Roberts @ 1999-05-11 0:00 UTC (permalink / raw) Well I've done a quick search on DN and nothing much came up (maybe it's too far back). I would be grateful if you would post a quick reprise of the arguments. ------------------------------------- Nick Roberts ------------------------------------- ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-11 0:00 ` Assertions Nick Roberts @ 1999-05-11 0:00 ` Robert Dewar 1999-05-12 0:00 ` Assertions Dale Stanbrough 0 siblings, 1 reply; 35+ messages in thread From: Robert Dewar @ 1999-05-11 0:00 UTC (permalink / raw) In article <37383efd@eeyore.callnetuk.com>, "Nick Roberts" <nickroberts@callnetuk.com> wrote: > Well I've done a quick search on DN and nothing much came up > (maybe it's too far back). I would be grateful if you would > post a quick reprise of the arguments. Here are some questions to answer: 1. Is an assertion a post condition that the compiler can rely on? 2. Can assertions have side effects 3. If assertions are off, are there still static semantic restrictions on assertions. There are others, but this is enough :-) --== Sent via Deja.com http://www.deja.com/ ==-- ---Share what you know. Learn what you don't.--- ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-11 0:00 ` Assertions Robert Dewar @ 1999-05-12 0:00 ` Dale Stanbrough 1999-05-12 0:00 ` Assertions Robert Dewar 0 siblings, 1 reply; 35+ messages in thread From: Dale Stanbrough @ 1999-05-12 0:00 UTC (permalink / raw) Robert Dewar wrote: "Here are some questions to answer: 1. Is an assertion a post condition that the compiler can rely on? 2. Can assertions have side effects 3. If assertions are off, are there still static semantic restrictions on assertions." One solution to the first questions (as suggested before) is to have two types of assertions. One is the "please check this condition at run time and don't do any optimisations based on what you may be able to deduce from this assert" and the other is "I know this condition is true, please use it to the fullest to provide any further optimisations that you can". The latter is of course used as a supplement to the type system. I'm not sure which of these Eiffel supports, but probably Anna (the Ada83 annotation toolkit) would fall into the 1st category. I view Q2 as being very much like the question "should functions have side effects". I would tend to say no for assertions, but obviously this would be hard for a compiler to check (and of course assertions have timing side effects, which could cause problems in a time critical program). Dale ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-12 0:00 ` Assertions Dale Stanbrough @ 1999-05-12 0:00 ` Robert Dewar 0 siblings, 0 replies; 35+ messages in thread From: Robert Dewar @ 1999-05-12 0:00 UTC (permalink / raw) In article <dale-1205990834030001@dale.bu.cs.rmit.edu.au>, dale@cs.rmit.edu.au (Dale Stanbrough) wrote: Just to be clear, I answered the request for a summary of issues, but I really feel any detailed discussion is too much of a rerun, so I won't post any further to this thread. I really did not want to start this thread up again :-) --== Sent via Deja.com http://www.deja.com/ ==-- ---Share what you know. Learn what you don't.--- ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-11 0:00 ` Assertions Robert Dewar 1999-05-11 0:00 ` Assertions Nick Roberts @ 1999-05-12 0:00 ` Tucker Taft 1999-05-12 0:00 ` Assertions Marin David Condic ` (2 more replies) 1 sibling, 3 replies; 35+ messages in thread From: Tucker Taft @ 1999-05-12 0:00 UTC (permalink / raw) Robert Dewar wrote: > > In article <3736F549.E3DDCDEB@pwfl.com>, > diespammer@pwfl.com wrote: > >but I think the "pragma Assert" got enough attention that other > > compiler vendors have implemented it as well, so it is > > becoming a common > > - if not standard - feature of the language. I'd expect to see > > it in some future revision of the ARM. > > I would not! I do not see that the fundamental problems that > caused Assert not to make it into the Ada 95 RM have been > solved. For a discussion of these problems, consult the archives > (we have had that thread at least once, probably more than once > in recent memory). Robert is right that there were long discussions on this, but I think they could still be resolved. Many of the Ada 95 compilers have an informally agreed-upon way of supporing pragma Assert already. It is often tough to formalize these informal agreements, but it can be done, especially when you have existing implementations, and motivation to allow "reasonable" uses of the feature to be portable. In any case, here is a strawman: pragma Assert(boolean_expression [, string_expression]); This pragma may appear anywhere a declaration or a statement may occur. If the check Assertion_Check is suppressed, this pragma has no effect. If the check Assertion_Check is not suppressed, this pragma's elaboration/execution is equivalent to the execution of: if boolean_expression then System.Assertions.Raise_Assert_Failure([""|string_expression]); end if; Anyway, this is a strawman, and I presume it will live up to its name. ;-) -- -Tucker Taft stt@averstar.com http://www.averstar.com/~stt/ Technical Director, Distributed IT Solutions (www.averstar.com/tools) AverStar (formerly Intermetrics, Inc.) Burlington, MA USA ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-12 0:00 ` Assertions Tucker Taft @ 1999-05-12 0:00 ` Marin David Condic 1999-05-12 0:00 ` Assertions Larry Kilgallen 1999-05-18 0:00 ` Assertions Richard D Riehle 2 siblings, 0 replies; 35+ messages in thread From: Marin David Condic @ 1999-05-12 0:00 UTC (permalink / raw) Tucker Taft wrote: > > In any case, here is a strawman: > > pragma Assert(boolean_expression [, string_expression]); > <snip for brevity> > I can imagine that there are any number of issues which might make it difficult to write a rigorous definition for the pragma. That said, I still don't think this is sufficient reason to leave it out of a future standard. If a large number of compilers are including the pragma anyway, then inclusion in the standard will at least mean *some* level of safety as to what the feature means/does. (Wait a minute! That sounds suspiciously like the argument for legalizing drugs: "Well kids are going to do it anyway, so at least this way we can make sure they are getting 'healthy' drugs!" I'm not so sure I like being on this side of the argument! :-) Where there are going to be difficult issues, there are always the weasel words "Implementation Defined". Side effects of the boolean expression? Implementation Defined! At least you'll have common syntax and chances are that whatever semantic differences exist in theory, in practice they will likely be "corner cases" or simply uncommon. (I've seen endless discussion of parameter passing rules, for example, yet never once encountered a situation in real-world code where it caused a problem. Either the code never got ported to a different compiler where behavior was different or, if it did get ported, the code was structured in such a way as to not rely on the obscure side-effects. Is the expression "a tempest in a teapot" relevant here?) Anyway - I think your definition is fine, as long as the appropriate "Implementation Defined" weasel words are thrown in when the objections come up. MDC -- Marin David Condic Real Time & Embedded Systems, Propulsion Systems Analysis United Technologies, Pratt & Whitney, Large Military Engines M/S 731-95, P.O.B. 109600, West Palm Beach, FL, 33410-9600 ***To reply, remove "bogon" from the domain name.*** Visit my web page at: http://www.flipag.net/mcondic ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-12 0:00 ` Assertions Tucker Taft 1999-05-12 0:00 ` Assertions Marin David Condic @ 1999-05-12 0:00 ` Larry Kilgallen 1999-05-12 0:00 ` Assertions Tucker Taft 1999-05-13 0:00 ` Assertions Nick Roberts 1999-05-18 0:00 ` Assertions Richard D Riehle 2 siblings, 2 replies; 35+ messages in thread From: Larry Kilgallen @ 1999-05-12 0:00 UTC (permalink / raw) In article <3739CECA.6A49865B@averstar.com>, Tucker Taft <stt@averstar.com> writes: > In any case, here is a strawman: > > pragma Assert(boolean_expression [, string_expression]); > > This pragma may appear anywhere a declaration or a statement may > occur. If the check Assertion_Check is suppressed, this pragma > has no effect. If the check Assertion_Check is not suppressed, > this pragma's elaboration/execution is equivalent to the > execution of: > > if boolean_expression then > System.Assertions.Raise_Assert_Failure([""|string_expression]); > end if; I would have expected: if NOT boolean_expression then since I would expect to say: pragma Assert(Expression_I_Expect_To_Be_True); Larry Kilgallen ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-12 0:00 ` Assertions Larry Kilgallen @ 1999-05-12 0:00 ` Tucker Taft 1999-05-13 0:00 ` Assertions Nick Roberts 1 sibling, 0 replies; 35+ messages in thread From: Tucker Taft @ 1999-05-12 0:00 UTC (permalink / raw) Larry Kilgallen wrote: > ... > I would have expected: > > if NOT boolean_expression then So would I ;-). Well, as I said, it was a strawman... > since I would expect to say: > > pragma Assert(Expression_I_Expect_To_Be_True); Yes, definitely, make that "if NOT boolean_expression then ..." > Larry Kilgallen -- -Tucker Taft stt@averstar.com http://www.averstar.com/~stt/ Technical Director, Distributed IT Solutions (www.averstar.com/tools) AverStar (formerly Intermetrics, Inc.) Burlington, MA USA ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-12 0:00 ` Assertions Larry Kilgallen 1999-05-12 0:00 ` Assertions Tucker Taft @ 1999-05-13 0:00 ` Nick Roberts 1999-05-17 0:00 ` Assertions Dale Stanbrough 1 sibling, 1 reply; 35+ messages in thread From: Nick Roberts @ 1999-05-13 0:00 UTC (permalink / raw) I would suggest that a pragma Assert expands to something like the following: if not boolean_expression then Ada.Exceptions.Raise_Exception( Ada.Assertions.Assert_Failure'Identity, "Test expression evaluated to False in a pragma Assert." & NL & "Page: " & Page & "Line: " & Line & NL & "File: " & Source_File_Name & NL & [""|string_expression]); end if; where NL is the implementation's code for a line break. Then there should be a package: package Ada.Assertions is Assert_Failure: exception [renames lower_level_exception]; end; I think it's also got to be made explicit that if a pragma Assert in the place of a declaration---in the declarative region of a certain block---raises an exception, that exception must be immediately propagated out of the block (and can never be handled inside the block). I would also suggest the following points. 1. There's no reason why the compiler should not be able to assume that any assertion's condition holds true, regardless of whether assertion checking is turned on or off. This would obviously be highly desirable, since, in many cases, it would allow optimising compilers to make optimisations they otherwise could not. The situation is analogous to other checks: if a check is turned off, and consequently an exception fails to be raised, the program's behaviour is undefined, and possibly highly erratic; if Assertion_Check is on (the default) the failure of an assertion's condition will always raise an exception (so the condition will certainly always hold as a post condition). 2. I don't see why assertions should not be allowed to have side-effects. Whether it would be wise, in practice, for an assertion to have side effects is another matter (to be left to the 'wisdom' of the programmer ;-). 3. If Assertion_Check is turned off, but the compiler can nevertheless detect (at compile time) that an assertion's condition will always fail (be False), it should still be entitled to raise an exception. Again, this is analogous to the other checks. In theory, the compiler should be entitled to continue checking any assertions it fancies. 4. A pragma Assert must not be evaluated by the elaboration of a preelaborated library unit. ------------------------------------- Nick Roberts ------------------------------------- ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-13 0:00 ` Assertions Nick Roberts @ 1999-05-17 0:00 ` Dale Stanbrough 1999-05-19 0:00 ` Assertions Nick Roberts 0 siblings, 1 reply; 35+ messages in thread From: Dale Stanbrough @ 1999-05-17 0:00 UTC (permalink / raw) Nick Roberts wrote: " 1. There's no reason why the compiler should not be able to assume that any assertion's condition holds true" But of course there is the rub - I certainly don't want this to be true -all the time-. I want some assertions to be genuinely tested, while others to be used as an adjunct to the type system (and thus the compiler can use it for optimisation purposes). E.g. an assertion that a cached bill-of-materials total cost is indeed the sum of all it's line items is something i want checked, whereas an assertion that "this pointer is a linear pointer type" (i think that's the notation that Henry Baker uses to describe linear dynamic data structures) would be a useful way to give info to the compiler, but extremely expensive (if indeed possible) to test. Dale ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-17 0:00 ` Assertions Dale Stanbrough @ 1999-05-19 0:00 ` Nick Roberts 1999-05-22 0:00 ` Assertions Dale Stanbrough 0 siblings, 1 reply; 35+ messages in thread From: Nick Roberts @ 1999-05-19 0:00 UTC (permalink / raw) Could you give, please, one or two further examples, in a little more detail? I (if no-one else!) would appreciate this. ------------------------------------- Nick Roberts ------------------------------------- Dale Stanbrough wrote in message ... [...] |I want some assertions to be genuinely tested, while others to be used |as an adjunct to the type system (and thus the compiler can use it for |optimisation purposes). [...] ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-19 0:00 ` Assertions Nick Roberts @ 1999-05-22 0:00 ` Dale Stanbrough 1999-05-22 0:00 ` Assertions Ray Blaak ` (2 more replies) 0 siblings, 3 replies; 35+ messages in thread From: Dale Stanbrough @ 1999-05-22 0:00 UTC (permalink / raw) Nick Roberts wrote: " Could you give, please, one or two further examples, in a little more detail? I (if no-one else!) would appreciate this." in response to my statement... |I want some assertions to be genuinely tested, while others to be used |as an adjunct to the type system (and thus the compiler can use it for |optimisation purposes). For an assertion that I would like tested... procedure Insert (Root : in out Tree; Item : Element) is -- insert into a binary search tree begin -- insertion code. ... pragma Assert (Balanced (Root)); -- test this, die if it fails end Insert; This assertion would cause an exception if the assertion failed (i.e. the semantics that Tucker Taft recently described). The compiler would not take advantage of this assertion to make any optimisations. For an assertion that could be used by the compiler to optimise the code pragma Enforce (X in 1..9 or X in 20..29); case X is when 1..10 => Something; when 20..29 => Something_Else; when others => Put_Line ("Whoops!"); end case; In this example, the compiler could remove the others clause. The "Enforce" (I don't think this is a good name, but I can't think of anything better) is used to extend the type system. One problem with the name "Assert" is that people have different views about what it actually means. Robert Dewar considers that "Assert" _should_ be able to be used for optimisation purposes. Dale ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-22 0:00 ` Assertions Dale Stanbrough @ 1999-05-22 0:00 ` Ray Blaak 1999-05-22 0:00 ` Assertions Robert Dewar 1999-05-22 0:00 ` Assertions Robert Dewar 1999-05-23 0:00 ` Assertions Nick Roberts 2 siblings, 1 reply; 35+ messages in thread From: Ray Blaak @ 1999-05-22 0:00 UTC (permalink / raw) I would suggest the name "Verify" for assertions intended to be runtime checks, and "Assume" for assertions intended to give info to the compiler. dale@cs.rmit.edu.au (Dale Stanbrough) writes: > For an assertion that I would like tested... [...] > pragma Assert (Balanced (Root)); > -- test this, die if it fails [...] > For an assertion that could be used by the compiler to optimise > the code > pragma Enforce (X in 1..9 or X in 20..29); [...] > The "Enforce" (I don't think this is a good name, but I can't > think of anything better) is used to extend the type system. > > One problem with the name "Assert" is that people have > different views about what it actually means. Robert Dewar > considers that "Assert" _should_ be able to be used for > optimisation purposes. -- Cheers, The Rhythm is around me, The Rhythm has control. Ray Blaak The Rhythm is inside me, blaak@infomatch.com The Rhythm has my soul. ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-22 0:00 ` Assertions Ray Blaak @ 1999-05-22 0:00 ` Robert Dewar 1999-05-23 0:00 ` Assertions Nick Roberts 0 siblings, 1 reply; 35+ messages in thread From: Robert Dewar @ 1999-05-22 0:00 UTC (permalink / raw) In article <ur9o9f95c.fsf@infomatch.com>, Ray Blaak <blaak@infomatch.com> wrote: > > I would suggest the name "Verify" for assertions intended to > be runtime checks, and "Assume" for assertions intended to > give info to the compiler. In any case, this thread should have adequately demonstrated that (a) this is quite a tricky subject (b) it is not easy to propose a solution that gets any kind of consensus agreement. This has always been the case when this issue has been discussed, so it is hardly surprising to see it happening again :-) --== Sent via Deja.com http://www.deja.com/ ==-- ---Share what you know. Learn what you don't.--- ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-22 0:00 ` Assertions Robert Dewar @ 1999-05-23 0:00 ` Nick Roberts 1999-05-24 0:00 ` Assertions Ray Blaak 1999-05-24 0:00 ` Assertions Dale Stanbrough 0 siblings, 2 replies; 35+ messages in thread From: Nick Roberts @ 1999-05-23 0:00 UTC (permalink / raw) Robert Dewar wrote in message <7i7ei9$93v$1@nnrp1.deja.com>... |In article <ur9o9f95c.fsf@infomatch.com>, | Ray Blaak <blaak@infomatch.com> wrote: |> |> I would suggest the name "Verify" for assertions intended to |> be runtime checks, and "Assume" for assertions intended to |> give info to the compiler. | |In any case, this thread should have adequately demonstrated |that | |(a) this is quite a tricky subject |(b) it is not easy to propose a solution that gets any kind of | consensus agreement. | |This has always been the case when this issue has been |discussed, so it is hardly surprising to see it happening again |:-) Robert is absolutely right on both points, of course. However, I don't actually recall anybody actually suggesting anything to the contrary. I, for one, never expected otherwise. Of course it's a tricky subject! Of course consensus is not going to be handed to us on a plate! However, I would suggest that we can, nevertheless, attempt to negotiate this tricky subject, and to persue a sufficient consensus. If people hadn't taken this attitude towards almost all aspects of the development of the Ada standard, there would never have been an Ada language at all. At this point, I think I can suggest five possible pragmas as candidates for a future revision of the Ada standard (and perhaps for prior de facto adoption): ============================================================ pragma Assume (Condition); pragma Verify (Condition); The Assume and Verify pragmas are allowed anywhere a declaration or a statement is allowed. When the pragma would be elaborated, if it were a declaration, or executed, if it were a statement, the pragma is said to be executed. For execution of the Assume pragma, the compiler is allowed, but not required, to test the Condition, but in either case is allowed to assume that the Condition is true for the purposes of optimisation. For execution of the Verify pragma, the compiler is required, unless suppression of Verify_Check applies, to test the Condition is true. If the suppression of Verify_Check applies, the compiler is allowed, but not required, to omit this test. In any case, the compiler is allowed to assume that the Condition is true for the purposes of optimisation. pragma Verify_Before_Call (Subprogram,Condition); pragma Verify_Before_Return (Subprogram,Condition); These two pragmas are allowed anywhere a declaration is allowed in the public part of a package specification. The Subprogram must be the name of a subprogram declared before the pragma in the same specification. The condition may contain the names of any of the parameters of the subprogram, as well as any entity that would normally be visible at the point of the pragma (but not any entity in the body of the subprogram). The Verify_Before_Call pragma causes the execution, with the same Condition, of an implicit Verify pragma just before the first declaration, or, if the subprogram has no declarations, as the only declaration, of the subprogram. The Verify_Before_Return pragma causes the execution, with the same Condition, of an implicit Verify pragma just after the evaluation of the return expression of a return statement in the subprogram, or just before the execution of a return statement in the subprogram which has no return expression. For both these pragmas, the meanings of the names in the Condition shall be interpreted at the place of the pragmas (not at the places of their implicit execution). For all four of these pragmas, if the test of the Condition is actually done, and it fails (evaluates to False), the predefined exception Program_Error is raised. (If this exception is raised by a pragma which takes the place of a declaration, the exception is immediately propagated out the innermost enclosing block, and is never handled by an exception handler inside this block.) [There is a new check for the Suppress pragma, Verify_Check.] pragma Parallel_Loop [(Loop_Name)]; This pragma is allowed anywhere a statement is allowed, but must apply to loop. With no parameter, this pragma applies to the innermost enclosing loop statement; otherwise this pragma applies to loop whose name is Loop_Name. The loop must have an iteration scheme of the 'for' variety, and this iteration scheme must not include the reserved word 'reverse'. The pragma Parallel_Loop allows the compiler to assume, for the purposes of optimisation, that the loop it applies to has the following property: execution of the iterations of the loop may be arbitrarily overlapping, and in any order, without changing the effect of the loop. The compiler is allowed, but not required, to test that the loop actually has this property; if such a test is done, and fails, the predefined exception Program_Error is raised. ============================================================ It may well be better to use 'Assert' throughout rather than 'Verify'. Comments please. Does this count as a stoneman? :-) I hope no-one objects to my throwing in the last pragma, but it seemed reasonably appropriate. Sorry, I must go now, my mum is expecting her cup of tea ;-) ------------------------------------- Nick Roberts ------------------------------------- ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-23 0:00 ` Assertions Nick Roberts @ 1999-05-24 0:00 ` Ray Blaak 1999-05-24 0:00 ` Assertions Dale Stanbrough 1 sibling, 0 replies; 35+ messages in thread From: Ray Blaak @ 1999-05-24 0:00 UTC (permalink / raw) "Nick Roberts" <nickroberts@callnetuk.com> writes: > pragma Assume (Condition); > pragma Verify (Condition); I would also allow optional description strings that would be part of the raised exception, accessible via Ada.Exceptions. Most importantly, the strings would be evaluated only if Condition is False: pragma Assume (Condition [, description]); pragma Verify (Condition [, description]); This would eliminate once and for all code like: if Debug and not Condition then Verify (False, "complicated string that should be evaluated only " & "when necessary: " & DescriptionOf (currentObject)); end if; > For all four of these pragmas, if the test of the Condition is actually > done, and it fails (evaluates to False), the predefined exception > Program_Error is raised. (If this exception is raised by a pragma which > takes the place of a declaration, the exception is immediately propagated > out the innermost enclosing block, and is never handled by an exception > handler inside this block.) I would suggest another exception name, so that one can distinguish the fact that a programmer-defined check failed, as opposed to a mistake in general. Maybe: Assertion_Error, or both Verification_Error and Assumption_Error. > It may well be better to use 'Assert' throughout rather than 'Verify'. > Comments please. Well, "Assert" gives rise to discussions as to what it really means, especially in comp.lang.ada :-). The idea is to side-step the issue by letting the programmer decide which type of assertion is desired. Whatever names are chosen should clearly reflect the intention. -- Cheers, The Rhythm is around me, The Rhythm has control. Ray Blaak The Rhythm is inside me, blaak@infomatch.com The Rhythm has my soul. ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-23 0:00 ` Assertions Nick Roberts 1999-05-24 0:00 ` Assertions Ray Blaak @ 1999-05-24 0:00 ` Dale Stanbrough 1 sibling, 0 replies; 35+ messages in thread From: Dale Stanbrough @ 1999-05-24 0:00 UTC (permalink / raw) Nick Roberts wrote: " pragma Parallel_Loop [(Loop_Name)]; This pragma is allowed anywhere a statement is allowed, but must apply to loop. With no parameter, this pragma applies to the innermost enclosing loop statement; otherwise this pragma applies to loop whose name is Loop_Name. The loop must have an iteration scheme of the 'for' variety, and this iteration scheme must not include the reserved word 'reverse'." This sounds good, but i really know next to nothing about this area. I would certainly recommend anyone to read up on HPF (High Performance Fortran) to get an idea on the issues that have been examined on this topic. I -think- from previous postings that there are some features in Ada that may prevent the level of parallelisation (sp?) that Fortran can achieve (specifically exceptions (and probably finalisation and Async abort)). Dale ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-22 0:00 ` Assertions Dale Stanbrough 1999-05-22 0:00 ` Assertions Ray Blaak @ 1999-05-22 0:00 ` Robert Dewar 1999-05-23 0:00 ` Assertions Nick Roberts 2 siblings, 0 replies; 35+ messages in thread From: Robert Dewar @ 1999-05-22 0:00 UTC (permalink / raw) In article <dale-2205990829190001@r1021c-20.ppp.cs.rmit.edu.au>, dale@cs.rmit.edu.au (Dale Stanbrough) wrote: > Nick Roberts wrote: > One problem with the name "Assert" is that people have > different views about what it actually means. Robert Dewar > considers that "Assert" _should_ be able to be used for > optimisation purposes. No! Not at all! I said nothing of the kind, go back and check my posts. I merely pointed out that there were many possible interpretations of Assert, and mentioned that this was an issue. I have been VERY careful in this thread not to express opinions, other than that it is not clear what Assert should do! Robert Dewar P.S. in fact I don't think it is easy, or even possible, to specify precisely what this means ("use for optimization purposes"), so someone would have to define it for me, before I could tell you whether it made sense to me or not! --== Sent via Deja.com http://www.deja.com/ ==-- ---Share what you know. Learn what you don't.--- ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-22 0:00 ` Assertions Dale Stanbrough 1999-05-22 0:00 ` Assertions Ray Blaak 1999-05-22 0:00 ` Assertions Robert Dewar @ 1999-05-23 0:00 ` Nick Roberts 2 siblings, 0 replies; 35+ messages in thread From: Nick Roberts @ 1999-05-23 0:00 UTC (permalink / raw) Dale Stanbrough wrote ... [...] |For an assertion that I would like tested... | | procedure Insert (Root : in out Tree; Item : Element) is | -- insert into a binary search tree | begin | -- insertion code. | ... | | pragma Assert (Balanced (Root)); | -- test this, die if it fails | | end Insert; | |This assertion would cause an exception if the assertion failed |(i.e. the semantics that Tucker Taft recently described). The |compiler would not take advantage of this assertion to make any |optimisations. Supposing we had, at some other point in your code: Order_Pudding(Cherry_Pie); Insert(Cocktail,Umbrella); if not Balanced(Cocktail) then Have_Another(Cherry_Pie); end if; [I'm also going to assume the program has no tasks (other than the main task), and no volatile objects.] The compiler could decide, at compile time, to forego the second serving of pudding at this point. It would still have to call Balanced; but only once, as part of the assertion inside the body of Insert. Of course, if suppression of assertions is allowed inside the body of Insert, AND the compiler decides to comply with this suppression, then the condition in the if...then here would have to be tested (and two cherry pies are a theoretical possibility). [Assuming the waiter is never clumsy (and always balances the cocktail after inserting an umbrella into it), the second pie will never happen, in practice, but the compiler probably can't know this.] I do not see how this kind of optimisation---based on an assertion---could ever be a problem. (Am I wrong?) ------------------------------------- Nick Roberts ------------------------------------- PS: I would like to take the opportunity here to thank the people who responded to my questions in this thread. I have found the discussion illuminating and stimulating. ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-12 0:00 ` Assertions Tucker Taft 1999-05-12 0:00 ` Assertions Marin David Condic 1999-05-12 0:00 ` Assertions Larry Kilgallen @ 1999-05-18 0:00 ` Richard D Riehle 1999-05-19 0:00 ` Assertions Nick Roberts 2 siblings, 1 reply; 35+ messages in thread From: Richard D Riehle @ 1999-05-18 0:00 UTC (permalink / raw) In article <3739CECA.6A49865B@averstar.com>, Tucker Taft <stt@averstar.com> wrote: >In any case, here is a strawman: > > pragma Assert(boolean_expression [, string_expression]); > In one of my JOOP columns I proposed going a little further, coming closer to the Eiffel model, pragma Pre_condition (boolean_expression [ ... ]); pragma Post_condition (boolean_expression [ ... ]); pragma Invariant (boolean_expression [ ... ]); with the further suggestion that we adopt Require, Ensure, and Invariant from the Eiffel language. One must be careful with assertions as pragmas. It is quite possible to declare a non-sensical assertion that is never detected by the compiler. When declaring assertions for a derivation class, one can construct a boolean expression that holds for the root of the class but fails for some derived type. This is a fundamental problem with assertions. The more conservative approach of Ada, in which every type is invariant tends to be more appropriate for safety-critical software. If there were some way to formally prove, through a software routine, that an assertion did not resolve to some completely silly set of propositions during the derivation process, we might be more inclined to depend on them. As things stand now, assertion pragmas, while a good idea on the surface, could easily create more problems than they solve. I think we need to proceed with some caution in this area. SPARK does take a very conservative approach with assertions. However, SPARK does not support extensible derivation classes. This eliminates one of the potential dangers of relying on assertions. Am I being too cautious here? Richard Riehle richard@adaworks.com http://www.adaworks.com ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-18 0:00 ` Assertions Richard D Riehle @ 1999-05-19 0:00 ` Nick Roberts 1999-05-19 0:00 ` Assertions Richard D Riehle 1999-05-20 0:00 ` Assertions stimuli 0 siblings, 2 replies; 35+ messages in thread From: Nick Roberts @ 1999-05-19 0:00 UTC (permalink / raw) Richard D Riehle wrote in message <7hqe7m$q7i@sjx-ixn1.ix.netcom.com>... [...] | pragma Pre_condition (boolean_expression [ ... ]); | pragma Post_condition (boolean_expression [ ... ]); What would these actually do that Assert would not? | pragma Invariant (boolean_expression [ ... ]); This construct (I think) could be replaced by an Assert repeated in several places. Would it be so useful as to be worthwhile? (Perhaps it would.) | with the further suggestion that we adopt Require, Ensure, and | Invariant from the Eiffel language. For those of us Eiffel non-cognoscienti, what do these do, please? | One must be careful with assertions as pragmas. It is quite | possible to declare a non-sensical assertion that is never | detected by the compiler. When declaring assertions for a | derivation class, one can construct a boolean expression that | holds for the root of the class but fails for some derived type. 'Twas ever thus. In all cases, the programmer must be as careful to put something sensible into an Assert as into the code proper. Assertions are certainly no panacea: sometimes the code to check up on a piece of code would be more complex to write than the code it's checking; sometimes there is no practical way to check up on it at all; M****y's L*w ensures that bugs can get into the checking code as easily as they can get into the code proper (and be just as much of a S*****g B****r to root out ;-). | This is a fundamental problem with assertions. The more conservative | approach of Ada, in which every type is invariant tends to be more | appropriate for safety-critical software. If there were some way | to formally prove, through a software routine, that an assertion | did not resolve to some completely silly set of propositions during | the derivation process, we might be more inclined to depend on them. | As things stand now, assertion pragmas, while a good idea on the | surface, could easily create more problems than they solve. I would be grateful if you would expand a little on this, perhaps giving an example or two. I apologise to those who don't wish to retread this well-trodden ground, but there some of us who missed the boat first time around, and need to retread it. ------------------------------------- Nick Roberts ------------------------------------- ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-19 0:00 ` Assertions Nick Roberts @ 1999-05-19 0:00 ` Richard D Riehle 1999-05-20 0:00 ` Assertions Ehud Lamm 1999-05-20 0:00 ` Assertions stimuli 1999-05-20 0:00 ` Assertions stimuli 1 sibling, 2 replies; 35+ messages in thread From: Richard D Riehle @ 1999-05-19 0:00 UTC (permalink / raw) In article <3742eba6@eeyore.callnetuk.com>, "Nick Roberts" <nickroberts@callnetuk.com> wrote: >Richard D Riehle wrote in message <7hqe7m$q7i@sjx-ixn1.ix.netcom.com>... >[...] >| pragma Pre_condition (boolean_expression [ ... ]); >| pragma Post_condition (boolean_expression [ ... ]); >| pragma Invariant (boolean_expression [ ... ]); >What would these actually do that Assert would not? A pre-condition test (Eiffel Require assertion) guarantees that a subprogram will not be entered unless the assertion is satisfied. It can, in some environments, be applied at the class/type level, but is more often at the subprogram level. An example of this assertion is the "barrier" on a protected entry. The barrier is a lot like a pre-condition since it also evaluates a boolean expression before we can begin execution of the routine. The barrier is not precisely identical to a pre- condition, but it should give you the general idea. A post-condition (Eiffel Ensure) guarantees that a certain set of circumstances will be true before exiting a subprogram. If the post-condition fails, an exception may be raised. An invariant is much as it might seem to be from its name. During the life of the entity given an invariant condition, the invariant must be true. The Require, Ensure, and Invariant conditions may be applied to a subprogram, a type, or a even some variable. The designer of Eiffel (who did not invent these ideas but incorporated them into the design of his language), calls this "design by contract." It is important to understand that this is a run-time contract. Many safety-critical software practitioners feel this is the wrong place to evaluate assertions. The SPARK language takes a more conservative approach to the same idea. Ada probably needs an approach somewhere between SPARK and Eiffel. >This construct (I think) could be replaced by an Assert repeated in several >places. Would it be so useful as to be worthwhile? (Perhaps it would.) The Require, Ensure, and Invariant are part of the contract and would appear in the package specification (in Ada) not in the code. The Ada package specification can already be thought of as some kind of contract. Because of that, reinforcing the contract with publicly defined assertions would make sense. The public assertions should state explicitly the place where the assertion applies. Therefore, pre-condition or post- condition would be a clear indication to the client of the contract. Assertions are independent of the implementing code. In Ada this would make especially good sense because of the full separation between the definition of what to do (specification) and implementing code to do it (body). We may want to modify the assertions without touching the algorithms. In fact, we probably want the assertions to be independent of the algorithms. Therefore, it makes sense to differentiate between assertions required to enter the routine, those require for successful completion, and those required to remain unchanged for the life of each entity in the design. I hope this helps to clarify the thinking behind some of my earlier points. Let me be clear that I am not interested in turning Ada into Eiffel. I am interested in seeing Ada learn from other language designs. I know that Tucker explored this idea in great depth during the design of Ada 95 and understands the pros and cons. He did not lightly dismiss the notion of pre-, post, and invariant conditions. It was a decision seriously studied and excluded from Ada 95 for very good reasons. Richard Riehle richard@adaworks.com http://www.adaworks.com ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-19 0:00 ` Assertions Richard D Riehle @ 1999-05-20 0:00 ` Ehud Lamm 1999-05-21 0:00 ` Assertions Robert Dewar 1999-05-20 0:00 ` Assertions stimuli 1 sibling, 1 reply; 35+ messages in thread From: Ehud Lamm @ 1999-05-20 0:00 UTC (permalink / raw) On Wed, 19 May 1999, Richard D Riehle wrote: > I hope this helps to clarify the thinking behind some of my earlier > points. Let me be clear that I am not interested in turning Ada into > Eiffel. I am interested in seeing Ada learn from other language designs. > I know that Tucker explored this idea in great depth during the design > of Ada 95 and understands the pros and cons. He did not lightly dismiss > the notion of pre-, post, and invariant conditions. It was a decision > seriously studied and excluded from Ada 95 for very good reasons. > Are there any documents about this design issue? I am very much interested in DBC ("design by contract"), which I think is one of the nicest ideas in SE. So why did Ada95 dismiss it? Ehud Lamm mslamm@pluto.mscc.huji.ac.il ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-20 0:00 ` Assertions Ehud Lamm @ 1999-05-21 0:00 ` Robert Dewar 1999-05-21 0:00 ` Assertions Ehud Lamm 0 siblings, 1 reply; 35+ messages in thread From: Robert Dewar @ 1999-05-21 0:00 UTC (permalink / raw) In article <Pine.A41.3.96-heb-2.07.990520114314.161678A-100000@pluto.mscc.h uji.ac.il>, Ehud Lamm <mslamm@mscc.huji.ac.il> wrote: > Are there any documents about this design issue? I am very > much interested in DBC ("design by contract"), which I think > is one of the nicest ideas in > SE. So why did Ada95 dismiss it? DBC is a methodology, which of course you can adopt in any language, and indeed Ada is quite well suited for this purpose. The issue of whether specific language features should be designed into the language to support DBC is a different one. It is of COURSE not the case that all elements of a DBC approach can be captured by Eiffel assert statements (as soon as you constrain the syntax and semantics of such assertions, you limit their applicability). Obviously some level of support for design contracts seems like a good idea. FOr example, an Ada package spec is exactly an interface contract. Are assertions a la Eiffel the right form? Not clear the answer is yes. There are MANY other similar constructions and a lot of design room here. But to think that Ada dismissed DBC just because it did not adopt the particular partial assertion language facilities of Eiffel misses the point I think. --== Sent via Deja.com http://www.deja.com/ ==-- ---Share what you know. Learn what you don't.--- ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-21 0:00 ` Assertions Robert Dewar @ 1999-05-21 0:00 ` Ehud Lamm 1999-05-21 0:00 ` Assertions Tucker Taft 0 siblings, 1 reply; 35+ messages in thread From: Ehud Lamm @ 1999-05-21 0:00 UTC (permalink / raw) On Fri, 21 May 1999, Robert Dewar wrote: > But to think that Ada dismissed DBC just because it did not > adopt the particular partial assertion language facilities > of Eiffel misses the point I think. > > Sure. But still two points. 1) I was responding to a claim that the issue of DBC was dicussed in the Ada95 design process. I just wondered whether any documents from this dicussion may be available. 2) I think having language support for DBC is a good thing. (I am not advoacting Eiffel, just the general claim.) It is much cleaner, more readable and most reliable to declare some set of assertions as being the invariant of an ADt, than to explicitly code a check for them at the end (etc.) of each routine that updates the ADT. Don't you agree? Sure, language support is not essential for DBC. But I think it has many advantages. Ehud Lamm mslamm@pluto.mscc.huji.ac.il ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-21 0:00 ` Assertions Ehud Lamm @ 1999-05-21 0:00 ` Tucker Taft 0 siblings, 0 replies; 35+ messages in thread From: Tucker Taft @ 1999-05-21 0:00 UTC (permalink / raw) Ehud Lamm wrote: > > On Fri, 21 May 1999, Robert Dewar wrote: > > > But to think that Ada dismissed DBC just because it did not > > adopt the particular partial assertion language facilities > > of Eiffel misses the point I think. > > > > > Sure. > > But still two points. > 1) I was responding to a claim that the issue of DBC was dicussed in the > Ada95 design process. I just wondered whether any documents from this > dicussion may be available. We discussed associating assertions with types. We didn't "dismiss" them, but rather decided at the time they were too complex for the perceived benefit. We came quite close to standardizing on a pragma Assert, and in fact most Ada 95 compilers have implemented such a pragma. Whether we can get it officially standardized over the next few years, or just "de facto" standardized remains to be seen. > 2) I think having language support for DBC is a good thing. (I am not > advoacting Eiffel, just the general claim.) It is much cleaner, more > readable and most reliable to declare some set of assertions as being the > invariant of an ADt, than to explicitly code a check for them at the end > (etc.) of each routine that updates the ADT. Don't you agree? > Sure, language support is not essential for DBC. But I think it has many > advantages. Bertrand Meyer has a very specific definition of design by contract which he associates closely with the Eiffel assertions/invariants. Ada certainly has linguistic support for design by contract in general, though not in the same way as Eiffel. In particular, every subtype constraint in Ada is a contract that is enforced at run-time. In addition, the fact that Ada physically separates spec from body, and visible part from private part, creates a number of very well-defined and configuration-manageable "contracts" that are compiler enforced. Personally, I find one of the greatest weaknesses of Eiffel (and Java) is that classes do not provide this physical separation into spec and body. The notion that you "extract" the spec from a class is counter to the idea that you have a well-defined contract. The contract is much stronger if it is physically separate from the implementation. In a business contract, I would never allow the supplier to be the "keeper" of the contract, where I would have to ask the supplier to "extract" the contract from the current implementation. None of the above is meant to say I don't see the value in assertions and invariants. However, I think in practice, the support that Ada already has for contracts is in many ways more valuable on a "day-to-day" basis, because the range constraints (and other constraints) are ubiquitous in a typical Ada program, providing contract enforcement on a line-by-line basis and at every subprogram call, and the physical separation of spec and body is valuable in every package. I would certainly not want to trade Ada's existing support for "contracts" for just having the explicit assertions provided by Eiffel. I would want both. The pragma Assert generally available in Ada compilers already provides a good portion of the power of explicit assertions and invariants. > Ehud Lamm mslamm@pluto.mscc.huji.ac.il -- -Tucker Taft stt@averstar.com http://www.averstar.com/~stt/ Technical Director, Distributed IT Solutions (www.averstar.com/tools) AverStar (formerly Intermetrics, Inc.) Burlington, MA USA ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-19 0:00 ` Assertions Richard D Riehle 1999-05-20 0:00 ` Assertions Ehud Lamm @ 1999-05-20 0:00 ` stimuli 1999-05-21 0:00 ` Assertions Richard D Riehle 1 sibling, 1 reply; 35+ messages in thread From: stimuli @ 1999-05-20 0:00 UTC (permalink / raw) In article <7hv6bb$1l9@dfw-ixnews6.ix.netcom.com>, Richard D Riehle <laoXhai@ix.netcom.com> wrote: > The Require, Ensure, and Invariant conditions may be applied to > a subprogram, a type, or a even some variable. The designer of > Eiffel (who did not invent these ideas but incorporated them into > the design of his language), calls this "design by contract." It > is important to understand that this is a run-time contract. Many > safety-critical software practitioners feel this is the wrong place > to evaluate assertions. The SPARK language takes a more conservative > approach to the same idea. Ada probably needs an approach somewhere > between SPARK and Eiffel. This isn't entirely true, although I think I understand your point. The Eiffel contract is not a run-time concept, it is a static property of correct Eiffel systems (read: correct Eiffel programs). How an Eiffel compiler goes about testing these is implementation dependant. In fact, they needn't actually be checked as they have null semantics within a correct program. It would be correct Eiffel for a compiler to check the validity of the assertions at compile time and a correct Eiffel program needn't check them at all. Now, given that a general theorem checker for Eiffel is, in practical terms, very unlikely, most Eiffel implementations perform runtime checks of the assertions. This is a useful tool for testing and debugging, but it is not the greater part of what assertions are. -- Jeffrey L. Straszheim stimuli@my-dejanews.com --== Sent via Deja.com http://www.deja.com/ ==-- ---Share what you know. Learn what you don't.--- ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-20 0:00 ` Assertions stimuli @ 1999-05-21 0:00 ` Richard D Riehle 1999-05-21 0:00 ` Assertions Robert Dewar 0 siblings, 1 reply; 35+ messages in thread From: Richard D Riehle @ 1999-05-21 0:00 UTC (permalink / raw) In article <7i2015$jut$1@nnrp1.deja.com>, stimuli@my-dejanews.com wrote: >In article <7hv6bb$1l9@dfw-ixnews6.ix.netcom.com>, > Richard D Riehle <laoXhai@ix.netcom.com> wrote: > >> The Require, Ensure, and Invariant conditions may be applied to >> a subprogram, a type, or a even some variable. The designer of >> Eiffel (who did not invent these ideas but incorporated them into >> the design of his language), calls this "design by contract." It >> is important to understand that this is a run-time contract. Many >> safety-critical software practitioners feel this is the wrong place >> to evaluate assertions. The SPARK language takes a more conservative >> approach to the same idea. Ada probably needs an approach somewhere >> between SPARK and Eiffel. > >This isn't entirely true, although I think I understand your point. >The Eiffel contract is not a run-time concept, it is a static property >of correct Eiffel systems (read: correct Eiffel programs). I agree that it is possible that some assertions might be checkable at compile time. Most pre-conditions and post-conditions I have seen have not looked like something that could be strictly checked by the compiler -- such things as ensuring that a variable never has a value of zero at run-time. On the other hand, I realize that the Eiffel contract does give the compiler the ability to do conformance checking through assertions and other mechanisms of the contract. This is part of the power of Bertrand's fundamental idea of "design by contract." > It would be correct Eiffel for a compiler >to check the validity of the assertions at compile time and a correct >Eiffel program needn't check them at all. Understood. We agree on this. >Now, given that a general >theorem checker for Eiffel is, in practical terms, very unlikely, >most Eiffel implementations perform runtime checks of the assertions. Yes, this is true. Moreover, we have not yet reached the level of sophistication in software practice where we can apply foolproof theorem checkers on large-scale computer programs. Even Ada does not lend itself to this kind of validity checking. >This is a useful tool for testing and debugging, but it is not the >greater part of what assertions are. My earlier point was that, Assertions, when focused on run-time checking, are not sufficient for safety-critical software development. That is why SPARK put emphasis on assertions that are always evaluated at compile time. Also, it is possible to formulate an assertion that is flawed. Granted, most assertions are simple boolean expressions. Consider, though a post-condition such as, Ensure count = old count + 1 and (P) or (Y and Z) or not P; Someone will find fault with this construct, but I am not interested in absolute correctness of logic at the moment. Most Eiffel developers are careful not to create potentially self-cancelling assertions. There is always someone who will not be so careful. Also, I would not be surprised to see an inherited post-condition in conflict with some new post-condition. Granted, Eiffel has a nice set of features for avoiding this kind of thing, but the discussion concerned implementing assertions in Ada via a pragma. I think it will take a pragma to set the assertions, as suggested, but it might require a pragma to _undefine_ such a pragma to prevent conflicts within a derivation class. The addition of a general assertion mechanism to Ada would please me greatly. I wonder if it is not more complicated than simply adding a few new pragmas. For example, will the assertion pragma on type T be inherited by every derivation in T'Class? This question alone should spawn a whole set of associated questions. In Eiffel this has been thought through carefully. Even so, I not absolutely certain, with my limited knowledge of Eiffel, that one cannot create the kind of errors in Eiffel I suggested in my earlier paragraph. I think this one reason the SPARK devotees are taking such a conservative approach to this subject. I am told this was a concern that prevented a generalized assertion feature from becoming part of the Ada 95 standard. Someone may correct me on this, but I recall a discussion with one of the distinguished reviewers during which I was told as much. I suppose the person with the best perspective on this is Tucker. It would be interesting to hear his view on the why's and wherefore's of excluding pre-, post, and invariant assertions from the Ada 95 standard. Richard Riehle richard@adaworks.com http://www.adaworks.com ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-21 0:00 ` Assertions Richard D Riehle @ 1999-05-21 0:00 ` Robert Dewar 0 siblings, 0 replies; 35+ messages in thread From: Robert Dewar @ 1999-05-21 0:00 UTC (permalink / raw) In article <7i27tt$hn@dfw-ixnews11.ix.netcom.com>, Richard D Riehle <laoXhai@ix.netcom.com> wrote: > I agree that it is possible that some assertions might be > checkable at compile time. That misses the point, Eiffel assertions are not about checking (either at compile time or at run time). They are formalized comments stating certain static properties of the program. If one of these comments lies, this is a bug in the program. One of course wants to debug programs, so mechanisms like testing assertions at run time etc are useful for debugging the assertions (as well as the rest of the code). But you really have to get out of the habit of thinking of them as having much to do with the check-this-assertion-at run-time type gizmo which is what most of this thread has been discussing. As I said earlier, assertions mean many different things to different people :-) --== Sent via Deja.com http://www.deja.com/ ==-- ---Share what you know. Learn what you don't.--- ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-19 0:00 ` Assertions Nick Roberts 1999-05-19 0:00 ` Assertions Richard D Riehle @ 1999-05-20 0:00 ` stimuli 1 sibling, 0 replies; 35+ messages in thread From: stimuli @ 1999-05-20 0:00 UTC (permalink / raw) In article <3742eba6@eeyore.callnetuk.com>, "Nick Roberts" <nickroberts@callnetuk.com> wrote: <snip adhoc ada versions of require/assure/invariant> > For those of us Eiffel non-cognoscienti, what do these do, please? These are the three main types of Eiffel assertions. For details, see: http://www.eiffel.com/doc/manuals/technology/contract/index.html -- Jeffrey L. Straszheim stimuli@my-dejanews.com --== Sent via Deja.com http://www.deja.com/ ==-- ---Share what you know. Learn what you don't.--- ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-10 0:00 Assertions J & A Richardson 1999-05-10 0:00 ` Assertions Marin David Condic @ 1999-05-12 0:00 ` Peter Amey 1999-05-12 0:00 ` Assertions Robert Dewar 1 sibling, 1 reply; 35+ messages in thread From: Peter Amey @ 1999-05-12 0:00 UTC (permalink / raw) J & A Richardson wrote: > > I have looked through the RM and can not find any refference to > assertions, pre conditions, or post conditions. > > It was my understanding that Ada 95 used assertions. > > I have also looked through a couple of webpages. > > Does Ada 95 use exceptions to work as assertions? Or am I missing > something? > The SPARK Ada subset has assertions in the form of pre/post conditions, loop invaraints etc. which are used to generate verification conditions (prrof obligations) allowing partial correctness to be established. These are not checks which are monitiored at run time. Peter -- --------------------------------------------------------------------------- __ Peter Amey, Product Manager ) Praxis Critical Systems Ltd / 20, Manvers Street, Bath, BA1 1PX / 0 Tel: +44 (0)1225 466991 (_/ Fax: +44 (0)1225 469006 http://www.praxis-cs.co.uk/ -------------------------------------------------------------------------- ^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: Assertions 1999-05-12 0:00 ` Assertions Peter Amey @ 1999-05-12 0:00 ` Robert Dewar 0 siblings, 0 replies; 35+ messages in thread From: Robert Dewar @ 1999-05-12 0:00 UTC (permalink / raw) In article <37397272.4B2FC372@praxis-cs.co.uk>, Peter Amey <pna@praxis-cs.co.uk> wrote: > The SPARK Ada subset Hmmm! I am very careful not to refer to SPARK as an Ada subset, since really it is a language in its own right, and I thought that was something Praxis liked to stress :-) > has assertions in the form of pre/post conditions, loop > invaraints etc. which are used to generate verification > conditions (proof obligations) allowing partial > correctness to be established. > These are not checks which are monitiored at run time. Indeed, this is yet a third view of assertions quite different from the other two (run time checks, or assertions for the compiler optimizer). I should have included this case in my summary questions. Assert is one of these things everyone thinks is a) a good thing b) straightforward till you begin to discuss it, and realize that different people have very different notions about what an assertion is! --== Sent via Deja.com http://www.deja.com/ ==-- ---Share what you know. Learn what you don't.--- ^ permalink raw reply [flat|nested] 35+ messages in thread
end of thread, other threads:[~1999-05-24 0:00 UTC | newest] Thread overview: 35+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 1999-05-10 0:00 Assertions J & A Richardson 1999-05-10 0:00 ` Assertions Marin David Condic 1999-05-11 0:00 ` Assertions Robert Dewar 1999-05-11 0:00 ` Assertions Nick Roberts 1999-05-11 0:00 ` Assertions Robert Dewar 1999-05-12 0:00 ` Assertions Dale Stanbrough 1999-05-12 0:00 ` Assertions Robert Dewar 1999-05-12 0:00 ` Assertions Tucker Taft 1999-05-12 0:00 ` Assertions Marin David Condic 1999-05-12 0:00 ` Assertions Larry Kilgallen 1999-05-12 0:00 ` Assertions Tucker Taft 1999-05-13 0:00 ` Assertions Nick Roberts 1999-05-17 0:00 ` Assertions Dale Stanbrough 1999-05-19 0:00 ` Assertions Nick Roberts 1999-05-22 0:00 ` Assertions Dale Stanbrough 1999-05-22 0:00 ` Assertions Ray Blaak 1999-05-22 0:00 ` Assertions Robert Dewar 1999-05-23 0:00 ` Assertions Nick Roberts 1999-05-24 0:00 ` Assertions Ray Blaak 1999-05-24 0:00 ` Assertions Dale Stanbrough 1999-05-22 0:00 ` Assertions Robert Dewar 1999-05-23 0:00 ` Assertions Nick Roberts 1999-05-18 0:00 ` Assertions Richard D Riehle 1999-05-19 0:00 ` Assertions Nick Roberts 1999-05-19 0:00 ` Assertions Richard D Riehle 1999-05-20 0:00 ` Assertions Ehud Lamm 1999-05-21 0:00 ` Assertions Robert Dewar 1999-05-21 0:00 ` Assertions Ehud Lamm 1999-05-21 0:00 ` Assertions Tucker Taft 1999-05-20 0:00 ` Assertions stimuli 1999-05-21 0:00 ` Assertions Richard D Riehle 1999-05-21 0:00 ` Assertions Robert Dewar 1999-05-20 0:00 ` Assertions stimuli 1999-05-12 0:00 ` Assertions Peter Amey 1999-05-12 0:00 ` Assertions Robert Dewar
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox