CVS difference for ais/ai-00286.txt

Differences between 1.7 and version 1.8
Log of other versions for file ais/ai-00286.txt

--- ais/ai-00286.txt	2003/06/18 00:12:23	1.7
+++ ais/ai-00286.txt	2003/07/03 04:37:46	1.8
@@ -1,4 +1,4 @@
-!standard 11.5 (00)                                03-03-05  AI95-00286/04
+!standard 11.5 (00)                                03-06-23  AI95-00286/04
 !standard 11.4.1 (10)
 !class amendment 02-02-05
 !status work item 02-02-05
@@ -673,6 +673,203 @@
 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.
 
 ****************************************************************
 

Questions? Ask the ACAA Technical Agent