!standard 11.5 (00) 04-02-28 AI95-00286/05 !standard 11.4.1 (10) !class amendment 02-02-05 !status work item 02-02-05 !status received 02-02-05 !priority Medium !difficulty Medium !subject Assert pragma !summary A standard "assert" pragma is proposed which takes a boolean expression and an optional string and raises Ada.Assertions.Assertion_Error if the expression evaluates to false. To control how the pragma is handled in the generated code, a configuration pragma "Assertion_Policy" is defined. !problem Several Ada compilers support an "assert" pragma, in largely the same form. This AI proposes to standardize the pragma, an associated package, and an associated configuration pragma for controlling the effect of the pragma on the generated code. It anticipates proposals for additional assertion-like pragmas for subprogram call pre and post conditions, and type and package oriented invariants. These will be discussed in separate AIs. !proposal The form of the pragma Assert is as follows: pragma Assert(boolean_expression[, [Message =>] string_expression]); A pragma Assert is allowed at the place where a basic_declaration or a statement is allowed. The package Ada.Assertions is as follows: package Ada.Assertions is pragma Pure(Ada.Assertions); Assertion_Error : exception; -- This exception is raised by an assertion check that fails procedure Assert(Check : in Boolean; Message : in String := ""); -- Calling this procedure has no effect if Check is true. -- It raises Assertion_Error if false, with the associated -- exception message if non-null. end Ada.Assertions; [Should we add the following (though how could you tell)? A compilation unit with an Assert pragma has a semantic dependence on the Ada.Assertions library unit.] The following configuration pragma is defined: pragma Assertion_Policy(assertion_policy_identifier); assertion_policy_identifier ::= Check | Ignore | implementation-defined-assertion_policy An Assertion_Policy pragma is a configuration pragma that specifies the assertion policy in effect for the compilation units to which it applies. Different policies may pertain to different compilation units within the same partition. An assertion policy specifies how an Assert pragma is interpreted by the implementation. If the assertion policy is "Ignore" at the point of an Assert pragma, the pragma is ignored. If the assertion policy is "Check" at the point of an Assert pragma, the elaboration of the pragma consists of evaluating the boolean expression, and if it evaluates to False, evaluating the Message string, if any, and raising the exception Ada.Assertions.Assertion_Error, with a message if the Message argument is provided. Other implementation-defined assertion policies might be introduced to specify that the compiler should perform static analysis presuming the assertions are true, even if code for the assertions is suppressed (i.e. it would be erroneous if they are false). These have not been standardized because specifying their semantics portably is problematic (and a bit controversial, to be honest). Calling the procedure Ada.Assertions.Assert is equivalent to: if Check = False then Ada.Exceptions.Raise_Exception( Ada.Assertions.Assertion_Error'Identity, Message); end if; except that it can be called from Pure code. The procedure Assert has these effects independent of the assertion policy in effect. NOTE: The boolean expression in an Assert pragma should normally not call functions that have side-effects (or at least, not when the result of the expression is True) so that the particular assertion policy in effect will not affect normal operation of the program. Implementation Permission Assertion_Error may be declared by renaming an implementation-defined exception from another package. !wording Add the following new section (and renumber the existing 11.4.2 to be 11.4.3): 11.4.2 Pragmas Assert and Assertion_Policy Pragma Assert is used to assert the truth of a boolean expression at any point within a sequence of declarations or statements. Pragma Assertion_Policy is used to control whether such assertions are to be ignored by the implementation, checked at run-time, or handled in some implementation-defined manner. Syntax The form of a pragma Assert is as follows: pragma Assert(boolean_expression[, [Message =>] string_expression]); A pragma Assert is allowed at the place where a basic_declaration or a statement is allowed. The form of a pragma Assertion_Policy is as follows: pragma Assertion_Policy(assertion_policy_identifier); assertion_policy_identifier ::= Check | Ignore | implementation-defined-assertion_policy A pragma Assertion_Policy is a configuration pragma. Static Semantics A pragma Assertion_Policy is a configuration pragma that specifies the assertion policy in effect for the compilation units to which it applies. Different policies may pertain to different compilation units within the same partition. The default assertion policy is implementation-defined. The following language-defined library package exists: package Ada.Assertions is pragma Pure(Ada.Assertions); Assertion_Error : exception; procedure Assert(Check : in Boolean; Message : in String := ""); end Ada.Assertions; A compilation unit containing a pragma Assert has a semantic dependence on the Ada.Assertions library unit. Dynamic Semantics An assertion policy specifies how a pragma Assert is interpreted by the implementation. If the assertion policy is Ignore at the point of a pragma Assert, the pragma is ignored. If the assertion policy is Check at the point of a pragma Assert, the elaboration of the pragma consists of evaluating the boolean expression, and if it evaluates to False, evaluating the Message string, if any, and raising the exception Ada.Assertions.Assertion_Error, with a message if the Message argument is provided. Calling the procedure Ada.Assertions.Assert is equivalent to: if Check = False then Ada.Exceptions.Raise_Exception( Ada.Assertions.Assertion_Error'Identity, Message); end if; except that it can be called from Pure code. The procedure Assertions.Assert has these effects independent of the assertion policy in effect. Implementation Permission Assertion_Error may be declared by renaming an implementation-defined exception from another package. Implementations may define their own assertion policies. AARM Implementation Note: Other implementation-defined assertion policies might be introduced to specify that the compiler should perform static analysis presuming the assertions are true, even if some or all of the code for the assertions is suppressed (i.e. it would be erroneous if they were false). NOTE 1: The boolean expression in an Assert pragma should normally not call functions that have side-effects when the result of the expression is True, so that the particular assertion policy in effect will not affect normal operation of the program. QUESTION: Should pragma Suppress(All_Checks); be a way to locally suppress a check of an assertion, even when the policy is "Check"? If so, do we need to mention that somewhere? (Note that the combination of policy "Check" and Suppress(All_Checks) could provide the effect of the "Assume_True" policy we discussed at one point.) !discussion This AI attempts to standardize the Assert pragma already supported by various implementations. The package and exception name are probably not the same as any existing implementation, but presumably exception and subprogram renaming can be used to provide backward compatibility. There was some concern expressed about the word "Assert" as implying an orientation toward static analysis, as opposed to run-time checking. However, there is a significant history of using "assert" for run-time checking in programming languages (cf. C, C++, Java, Eiffel), and a number of existing Ada compilers have adopted the term as well, so it seems that that "cat" is already well out of the "bag." We considered using pragma Suppress to control the affect of the Assert pragma, but it was felt that this could lead to confusion, as pragma Suppress can always be ignored by the implementation, whereas one possible desired interpretation for pragma suppress of assertions is that they are certain to be completely ignored. The configuration pragma approach gives more flexibility, and allows the user to be explicit as to how the pragmas are to be interpreted. For those wanting run-time checking, Check makes the most sense. Ignore ensures that adding an Assert pragma can never make the program less safe. Other implementation-defined policies can be defined which might be more oriented toward static analysis. We originally proposed two other language-defined assertion policies, Assume_True and Evaluate_And_Assume_True. However, these both could result in erroneous execution, and might not match what would be most useful for static analysis in any case, hence we leave it to implementations to provide other policies as they see fit. Because configuration pragmas can be separated off into a single file, having implementation-defined policies should not endanger the portability of the bulk of an application that uses Assert pragmas. We have provided a procedure Assert as well, as it is something that could be used on compilers that don't yet support the pragma, and it eliminates any possibility of the assertion policy affecting the operation of the program. We considered providing a pragma Assertions_Only to address the concern that to make assertion pragmas most valuable, additional operations or objects may need to be defined. This pragma would ensure that these additional constructs are only referenced from within assertion pragmas or other Assertions_Only constructs. Implementations would be encouraged to minimize storage occupied by such constructs if assertion policy Ignore applies to all compilation units with visibility on the construct. Note that there would be no permission to eliminate elaboration of such constructs or the side-effects associated with this elaboration. However, an implementation-defined assertion policy might be used to control aspects of Assertion_Only constructs further. In any case, we have moved that proposal into a separate AI (AI-374) to avoid confusing the issue with this one. Here are comments on other issues identified by the HRG: 1) Limitations on expressiveness We believe that Ada is fully capable of expressing almost anything of interest. The System_Of_Units AI provides some examples of using pragma Assert with relatively sophisticated expressions. However, we realize it may be necessary to introduce additional variables or functions. We believe that something like an "Assertions_Only" pragma could be used to identify clearly these additional variables or functions, and to enable the implementation to minimize storage devoted to them when assertions are being ignored. See the Assertions_Only AI which attempts to address this concern. Specific mention is made of implication and quantifiers. Both of these can be readily defined in Ada: Implication can be defined using a rename: function Implies(A, B : Boolean) return Boolean renames "<="; Quantification would require defining appropriate functions, perhaps with the help of appropriate generics. Again, somthing like an Assertions_Only pragma could be used if storage space were a concern. 2) The possibility of side-effects. This seems entirely within the programmers control. By judicious use of pragma Pure, this problem can be minimized. An additional policy could be defined which required all expressions in a pragma Assert to be pure. 3) The use of exceptions. Exceptions are the way in which errors are signaled in Ada. Yes it is possible to catch them by mistake by using "when others," but that is as true for Constraint_Error as it is for Assertion_Error. Clearly in a high-integrity system, there is often a desire to eliminate all exceptions. This is generally done by certifying either statically or through heavy testing that the exceptions will not be raised. An advantage of pragma Assert is it allows the programmer to specify explicit checks that are treated essentially like the language-defined checks, and would require the same level of proof. 4) The use of the word "assert." That was discussed above. One main underlying objection seems to be that the pragma Assert might not be terribly useful for high-integrity systems. Although we believe that they can be just as useful as the language-defined run-time checks, namely they provide a set of additional explicit "checks" which must be "proved" safe by testing or analysis, we don't believe that pragma Assert should go in annex H. We believe it is a generally useful capability, that is already in wide use, and should be standardized, and probably defined somewhere in chapter 11 (exceptions). !example !ACATS test ACATS(s) tests need to be constructed to test this feature. !appendix From: Robert Dewar Sent: Wednesday, February 6, 2002, 2:40 PM I doubt we would implement this in its suggested form, because it is very close to what we have but arbitrarily different, and I would see no reason to disconcert our existing customers who use this feature with such small changes. The package in GNAT is: package System.Assertions is Assert_Failure : exception; -- Exception raised when assertion fails procedure Raise_Assert_Failure (Msg : String); pragma No_Return (Raise_Assert_Failure); -- Called to raise Assert_Failure with given message end System.Assertions; This package has been in use by many of our customers since 1993, and I see no benefit to them in making arbitrary small changes to this spec. **************************************************************** From: Tucker Taft Sent: Wednesday, February 6, 2002, 3:20 PM I mentioned this issue in the AI, and suggested that with renaming of exceptions and subprograms, backward compatibility could be achieved. Is there a reason why the renaming wouldn't work adequately? **************************************************************** From: Robert Dewar Sent: Wednesday, February 6, 2002, 4:03 PM Yes that might work fine **************************************************************** From: Alan Burns Sent: Tuesday, January 7, 2003, 5:01 AM he HRG was asked (by ARG) to look at these AIs on assert and pre/post conditions etc. Please find attached our considerations (which was on the whole are not supportive). To prevent these thoughts getting lost, perhaps they should be incorporated into the AIs ---- Comment from the HRG on AI286 - pragma Assert. The proposal contains a number of problems that clearly suggest that the AI does not in fact significantly aid the construction and verification of high-integrity software. At best, the proposed mechanism would provide a convenient debugging aid for use during program development. There are 4 particular difficulties, 3 of which are significant to the behaviour of Ada programs and the last which is more conceptual and stylistic: 1. Serious limitations to what can be expressed in the predicate associated with the pragma (i.e. what can be "asserted"). 2. The likelihood of program semantics being affected by the presence of assert pragmas and by the assertion policy in force. 3. The use of the exception mechanism to indicate assertion failure. 4. The use of the word "assert", which has strong connotations of proof for what is actually a "run time check". Limits on what can be Expressed ------------------------------- The proposed pragma allows for a standard Boolean expression or predicate. This limits assertions to what can expressed in the standard expression language of Ada. Furthermore, it means that assertions can only be made about program entities that are visible at the point where the assertion is to be planted. Unfortunately, many (perhaps most) of the interesting properties that it is worth asserting cannot be expressed in simple Ada expressions and/or involve program properties not visible according to the rules of Ada. Specific limitations in the expressions include: 1. a way of distinguishing current from initial variable values; 2. a notation for handling updates of structured variables; 3. the absence of implication operators; and 4. the absence of quantifiers. Examples: 1. We call an "Exchange" procedure and wish to assert that the parameter values have been exchanged: procedure Swap (X, Y : in out Integer); -- exchanges X and Y ... Swap (P, Q); pragma Assert (P = 'old value of Q', "Swap failure"); 2. We update the 3rd element of an array and wish to assert that the array is unchanged except for the new value: A (3) := X; pragma Assert (A = 'the old A with the 3rd element overridden by X', ... 3. We obtain the maximum of X or Y: Z := Max (X, Y); pragma Assert ('X > Y -> Z = X and X <= Y -> Z = Y', ... (admittedly this could be restructured to avoid the use of implication but many common forms of predicate are substantially clearer when expressed in the form shown). 4. We wish to assert that an array contains at least on element greater than 10. pragma Assert ('there exists in A some index value I such that (A(I) > 10, ... 5. We wish to assert that a stack is not full before calling a push operation; however, the stack package does not export an "IsFull" function and we don't want make the internals of the stack visible at the point of call. Effect of assertions on program semantics ----------------------------------------- The expression language used in the assertions allows the use of calls to functions which have side effects. This clearly allows the semantics of a program to be affected by the assertion policy in force. The AI admits this and even provides an option to evaluate the predicate ("for its side-effects") whilst ignoring the result. The paragraph stating that "...expression in an Assert pragma should normally not call functions that have side-effects...." is far too weak for a proposal that purports to raise the integrity of Ada programs. Use of exceptions ----------------- The raising of Assertion_Error as a mechanism for signalling assertion failures is highly problematic. 1. The exception may be inadvertently caught by an existing "when others" clause which would negate the purpose of the assertion mechanism. 2. The HRG report is cautious about the use of exceptions in high- integrity systems and the deliberate introduction of a new exception runs counter to the advice given in TR 15942. 3. Many high-integrity systems are built on reduced run-time systems that provide limited or no support for exception handling. Therefore, assertion checks would most likely have to be removed from production code; this reinforces the view that the proposal is more a debugging aid than a serious production tool. Use of term "Assert" -------------------- The term "assertion" has great significance to the program verification community. For most practitioners it implies the use of some form of proof process; however, the AI is proposing a run-time executable check which is semantically no different from "if C then raise X; end if". There is a serious risk of muddying the distinction between static proof work and testing/debugging. The HRG report itself takes great care to separate these different forms of verification. For these reasons, if the AI is accepted it is the HRG's view that this be on the basis that the pragma is renamed "Run_Time_Assert" or better "Run_Time_Check". Conclusions ----------- The weaknesses identified above reduce the AI to a simple debugging aid that offers no significant gain over what can currently be achieved using standard Ada language constructs. If the only purpose of the AI is to support high integrity systems (ie. if the pragma would be defined in Annex H) then the HRG does not support its acceptance. **************************************************************** From: Dale Stanbrough Sent: Friday, May 23, 2003, 8:40 AM Hello, I hope i have the format for the following AI proposal correct. If you have any questions, please feel free to contact me. The format (and some of the wording) has been taken from AI-286. Dale Stanbrough Director Adasoft (Australia). --------------------------------------------------------------------- !summary Two pragmas similar to "assert" are proposed which have slightly different semantics. !problem The exact semantics of pragma Assert are hard to define. It may result in a run time check, but compilers could also assume that the condition is true, and take advantage of it to make optimisations (and potentially remove other checks or code). This AI proposes that two pragmas, pragma Verify and pragma Assume, be created to separate the two possible uses of pragma Assert. !proposal The form of the pragma Verify is as follows: pragma Verify(boolean_expression[, [Message =>] string_expression]); A pragma Verify is allowed at the place where a basic_declaration or a statement is allowed. The form of the pragma Assume is as follows: pragma Assume(boolean_expression); A pragma Assume is allowed at the place where a basic_declaration or a statement is allowed. As per AI-286 the package Ada.Assertions is as follows: package Ada.Assertions is pragma Pure(Ada.Assertions); Assertion_Error : exception; -- This exception is raised by an assertion check that fails end Ada.Assertions; Pragma Assume specifies a boolean expression which the developer has proven to be true by analysis of the code. The purpose of the pragma is to provide extra information to the compiler to allow it to make optimisations in the generated code, as well as helping to document the code. There would be no evaluation of the boolean expression at run time, and therefore no possible raising of an exception. Pragma Verify would specify a boolean condition that is to be converted into a run time check that would raise Assertion_Error when it evaluates to false. It provides identical functionality to the pragma Assert provided by several compilers, but it would not be used to provide any optimisations of the code, and could therefore always be relied on to be checked at run time. Implementation Permission Assertion_Error may be declared by renaming an implementation-defined exception from another package. !wording !discussion !example !ACATS test !appendix From: John Barnes Sent: Tuesday, June 10, 2003 2:11 AM There is some disquiet in the UK concerning the possible interaction between the assert pragma proposed by AI-286 and the assert statement in Spark. After discussion among members of the UK BSI Ada panel, I have been asked to submit the following comment/suggestion. === The current AI286 suggests a new pragma "Assert" and a procedure Ada.Assertions.Assert for run-time assertion checking. However, there will be occasions where SPARK users will want to use both SPARK "static asserts" and pragma/procedure-based dynamic asserts in the same program. Unfortunately, this won't work given then current AI, since "assert" is a reserved word in SPARK. Any attempt to use this pragma simply generates a syntax error from the Exainer, which is most unfortunate. It is also impossible to write a legal SPARK shadow of the proposed Ada.Assertions package as is currently written. We suggest renaming the pragma and procedure to "Dynamic_Assert" or "Runtime_Assert" to avoid name-space conflict. These names also help to distinguish between dynamic asserts, and static asserts - an orignal concern of the HRG. === I believe that the HRG hopes to look at this again before the ARG meeting in Toulouse. The feeling about this AI is strong and I think I should add that unless it is amended to overcome this concern then it is probable that the UK will vote against it. **************************************************************** From: Robert Dewar Sent: Tuesday, June 10, 2003 2:27 AM I object to this renaming. First, there is nothing to stop a pragma from having the same name as a keyword if you are in the language extension business. Second I don't think we should choose a less convenient name (and for many many users of Ada 95 the name they have used extensively for ten years) just because some non-Ada compiler has an incompatible extension. My recommendation is fix the examiner so that it allows both the current use of the assert keyword, and also allows pragma assert. This is convenient in any case for using the examiner with existing compilers that recognize pragma Assert. **************************************************************** From: Alan Burns Sent: Tuesday, June 10, 2003 2:55 AM The HRG's concern with the use of `assert' was not a concern about name clash with SPARK examiner but with the widely held view in the verification world that `assert' implies a static provable property of a program not a wish that at run-time this property is true. Hence the HRG's view is that another name be used for the dynamic case. Please see HRG's earlier review of this AI **************************************************************** From: Pascal Leroy Sent: Tuesday, June 10, 2003 4:02 AM > I object to this renaming. I strongly agree with Robert here. 1 - Two major implementations have been supporting this pragma for years, and in fact the ARG careful designed AI 286 is such a way that incompatibilities would be minimized. Although we don't know for sure, chances are that there is a substantial amount of code out there that depends on these pragmas. Changing the name would defeat the purpose of the AI, which was to increase portability by making it possible to port code that includes assertions from one compiler to another. Not to mention that we would now have two assertion pragmas around, with just more confusion for the user. 2 - Anyone designing extensions to syntax of the language is in a state of sin, and should not be surprised that some of these extensions would conflict with future evolutions of the language, especially if they use perfectly good words like "assert". If I were designing an extension, I would choose a syntax that cannot possibly conflict with the rules of Ada, e.g. "_assert" (sounds like C, doesn't it). 3 - I understand the HRG concern, but it carries little weight in my opinion. The fact that a name conveys a meaning that may not be exactly right for some subcommunity of Ada users is no justification for introducing the compatibility mess described in #1. I would be happy to study proposals regarding pragmas for static checks (although that seems like a can of worms IMHO) but this is no justification for renaming Assert. **************************************************************** From: Tucker Taft Sent: Tuesday, June 10, 2003 8:58 AM Let me add my voice to the other implementors. This pragma has been supported for years by several vendors (Aonix, Green Hills, ACT, Intermetrics/AverStar/AverCom/SofCheck (do we count as 4? ;-), and probably others). It is silly to change the name at this point. Programmers certainly understand what it means, and "assert" is used in C, C++, Java, etc. Fixing the SPARK examiner to allow Assert in a pragma could not be more than an afternoon's work, given their impressive track record. The same "trick" that is used for attributes could be used here, namely if ASSERT is a reserved word, then change the pragma grammar rule to be: pragma ::= PRAGMA identifier [pragma_args]; | PRAGMA ASSERT pragma_args;" I really hope the UK delegation can understand the sense in standardizing this wide-spread existing practice, rather than inventing some new name. Certainly in the kind of code we develop in Ada, pragma Assert appears thousands of times. **************************************************************** From: Robert Dewar Sent: Wednesday, June 25, 2003 4:14 PM > The HRG's concern with the use of `assert' was not > a concern about name clash with SPARK examiner but > with the widely held view in the verification world > that `assert' implies a static provable property > of a program not a wish that at run-time this > property is true. > > Hence the HRG's view is that another name be used for > the dynamic case. > > Please see HRG's earlier review of this AI Well this might be a widely held view in the verification world but the use of assert for dynamic assertions is pretty well established in the more general programming language world. A huge amount of Ada is being written now using pragma Assert. Choosingt some other peculiar name at this stage will simply be regarded as peculiar by many Ada programmers, and for sure in the GNAT world, people will likely continue using Assert anyway, since its usage is so well established already. **************************************************************** From: Robert Dewar Sent: Wednesday, June 25, 2003 4:16 PM > The HRG's concern with the use of `assert' was not > a concern about name clash with SPARK examiner but > with the widely held view in the verification world > that `assert' implies a static provable property > of a program not a wish that at run-time this > property is true. One problem with the above viewpoint is that the issue of whether a property is provable or not is not a well defined predicate, it depends on how clever you are at proving things. Surely you don't think the standard should try to resolve *that* issue. In fact virtually all pragma Assert's in typical GNAT programs indeed DO refer to statically provable properties, just not ones that typically limited proof tools can actually prove :-) **************************************************************** From: Robert Dewar Sent: Wednesday, June 25, 2003 4:18 PM > 1 - Two major implementations have been supporting this pragma for > years, and in fact the ARG careful designed AI 286 is such a way that > incompatibilities would be minimized. Although we don't know for sure, > chances are that there is a substantial amount of code out there that > depends on these pragmas. Changing the name would defeat the purpose of > the AI, which was to increase portability by making it possible to port > code that includes assertions from one compiler to another. Not to > mention that we would now have two assertion pragmas around, with just > more confusion for the user. I gather from this that Rational implements pragma Assert, which indeeds strengthens the argument *considerably*. Sorry for not being aware of this. I must say that I found the original reluctance to include a pragma Assert a remarkable case of best being an enemy of good. The simple pragma Assert implemented in GNAT is immensely useful, and the name is indeed the most obvious name for a programmer (even if there were not years of time, and millions of lines of legacy code assuming this name). It is too bad that esoteric discussions about the deep meaning of assertions derailed putting in this simple pragma in the 95 standard. At this stage there are three things that 0X can do 1. Do nothing 2. Add pragma Assert 3. Add some new pragma with a peculiar name 1 and 2 are actually pretty similar in that for most Ada programmers they will have identical effect. I would prefer 2, but 1 is quite fine for me. 3 is actively confusing! **************************************************************** From: Robert Dewar Sent: Wednesday, June 25, 2003 10:43 PM > I really hope the UK delegation can understand > the sense in standardizing this wide-spread existing > practice, rather than inventing some new name. > Certainly in the kind of code we develop in Ada, > pragma Assert appears thousands of times. Another statistic, in the GNAT compiler and run time, pragma assert occurs just under 4000 times. **************************************************************** From: John Barnes Sent: Thursday, June 26, 2003 1:46 AM Although it wasn't really discussed at the ARG meeting, there have been further private discussions as a consequence of whch the UK withdraws its comment. **************************************************************** From: Robert Dewar Sent: Thursday, June 26, 2003 7:57 AM Thanks for the note. Sorry to beat a dead horse, but I could not see evidence of its demise :-) :-) **************************************************************** From: Alan Burns Sent: Thursday, June 26, 2003 2:31 AM The ARG did not get to talk about AI-286 at its last meeting. The HRG has discussed the newly worded AI again and is more positive. We note the different uses of `assert' and realise that there is no simple answer to this - but as the pragma is being defined in Chapter 11 (not Annex H) then the HRG is not going to object if the name Assert is used. **************************************************************** From: Alan Burns Sent: Thursday, June 26, 2003 2:34 AM > Another statistic, in the GNAT compiler and run time, pragma assert occurs > just under 4000 times. How often do they fail? :-) **************************************************************** From: Robert Dewar Sent: Thursday, June 26, 2003 8:06 AM Early on, we delivered the GNAT compiler with assertions enabled, and most compiler bugs showed up as failed assertions. Now, we have assertions turned off in the delivered version, and so they don't fail in production circumstances (and at this stage, the kind of bug that causes such failures is much more rare), but internally during development we still find them extremely useful, almost essential. I can certainly say that development of GNAT without assertions would have been very much harder. **************************************************************** From: Robert A Duff Sent: Thursday, June 26, 2003 8:07 AM > How often do they fail? :-) I see the smiley, but anyway: My current project at SofCheck is a tool for proving assertions and the like at "compile" time (i.e. statically). In the source code of this tool, about 1% of the lines of code are pragmas Assert. (By comparison, 15% of the lines are blank, and 18% are or contain comments.) I think the 1% figure is roughly the same as what Robert reported for the GNAT sources, if I remember its size correctly. My experience is that failures of pragma Assert are the most common symptom of bugs at run-time. More common even than Constraint_Error. And far more common that wrong answers. Unfortunately, the tool is not quite ready to analyze itself! I'm not trying to prolong the argument about the name of the pragma, since that seems pretty well settled. I just thought these statistics were interesting. **************************************************************** From: Pascal Leroy Sent: Friday, June 27, 2003 7:18 AM To add another data point, our compiler has about 1.1MSLOCs total, with 11% blank lines and 15 % comments. We have about 2300 pragmas Assert, which is a bit more than 0.2%. I didn't do precise statistics, but I'd say that, of the defects that I see, about one third are Assertion_Errors, one third are Constraint_Errors, and the remaining third are miscellaneous errors. **************************************************************** From: Robert C. Leif Sent: Sunday, February 1, 2004 12:31 AM The following is from 03-06-23 AI95-00286/04. Evidently the status is a work item for Ada 0Y The following configuration pragma is defined: pragma Assertion_Policy(assertion_policy_identifier); assertion_policy_identifier ::= Check | Ignore | implementation-defined-assertion_policy Since at SIGAda 2003 SPARK was demonstrated to be a useful and potentially the killer technology for Ada, it would be prudent to include the possibility of enhancing Ada to do the equivalent of SPARK. Since SPARK is a compile time tool that heavily uses assertions, Ada 0Y should include a standardized means to call compile time assertions. However as far as I know, compile time assertions have never been implemented in a standard Ada compiler. Therefore, the syntax for this option should be specified and the implementation should NOT be required. The possibilities should be expanded in Assertion_Policy: Run_Check, Compile_Check, and Run_And_Compile_Check. The new definition would be: pragma Assertion_Policy(assertion_policy_identifier); assertion_policy_identifier ::= Run_Check | Compile_Check | Run_And_Compile_Check | Ignore | implementation-defined-assertion_policy **************************************************************** From: Jean-Pierre Rosen Sent: Sunday, February 29, 2004 3:04 AM There seems to be a contradiction here... > procedure Assert(Check : in Boolean; Message : in String := ""); > -- Calling this procedure has no effect if Check is true. > -- It raises Assertion_Error if false, with the associated > -- exception message if non-null. [...] > if Check = False then > Ada.Exceptions.Raise_Exception( > Ada.Assertions.Assertion_Error'Identity, Message); > end if; If I understand correctly the first statement, it is rather equivalent to: if Check = False then if Message = "" then raise Assertion_Error; else Ada.Exceptions.Raise_Exception( Ada.Assertions.Assertion_Error'Identity, Message); end if; end if; i.e. if Message is "", it should give the predefined message **************************************************************** From: Robert Dewar Sent: Monday, March 1, 2004 6:50 PM That seems wrong, I think if Message is "" then you should get an implementation dependent string (in GNAT, it is the source location of the failure, which 99.999% of the time is all you want anyway). ****************************************************************