CVS difference for ais/ai-00288.txt

Differences between 1.2 and version 1.3
Log of other versions for file ais/ai-00288.txt

--- ais/ai-00288.txt	2003/01/03 00:01:36	1.2
+++ ais/ai-00288.txt	2003/01/24 04:14:27	1.3
@@ -621,3 +621,139 @@
+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 AI288 - Pre/Postconditions and Invariants
+The AI proposes the extension of the assertion mechanism (AI286) to
+provide support for "programming by contract".  Specifically it provides
+a mechanism to express pre and postconditions for operations and
+statements about invariant properties of types and packages.
+As with AI286, the fundamental question to be answered is "does the
+proposal aid the construction and verification of high-integrity,
+software-driven systems"?
+The proposal has a number of problems that, in the HRG's opinion,
+results in a negative answer to this question.
+In particular, as presented, the AI describes a mechanism that is
+more suitable for debugging than constructing a system "by contract".
+The author appears to recognise this by stating its aim as: "to ... catch
+errors in usage or implementation earlier in the development cycle".
+Specific weakness in the proposal include the following:
+1.  It is built on the Assert mechanism proposed in AI286 and
+shares all the problems associated with that AI.  Indeed, some of those
+weaknesses are more severe if assert is to be employed in the
+way proposed.  In particular, the desire to promote the contract to
+package specifications is fundamentally incompatible with the visibility
+rules of Ada.  How, for example, will the invariant condition of an
+abstract state machine package be expressed in its specification if the
+data to which the invariant applies is, correctly, hidden in the package
+body?  Only a proliferation of extra functions (perhaps with side-
+effects?) can be employed.
+2. Although the attribute "incoming" provides the initial value of
+parameters that are imported and exported by an operation, there is no
+equivalent mechanism for global variables used by the operation. This
+makes it impossible to express pre and post conditions that rely on the
+initial values of global variables.  Since such globals may well be
+invisible at the point where the pre/post condition is being expressed,
+this deficiency may well be insoluble.
+Trivial example:
+X : Integer;
+procedure Inc is
+  X := X + 1;
+end Inc;
+The postcondition of Inc, "X = X'Incoming + 1, cannot be expressed.
+Furthermore, the value X'Incoming cannot be provided by the compiler
+because, unlike a parameter which has its mode, we don't know whether a
+global is referenced or updated until we reach the sequence of
+statements in the subprogram body. The initial value could only be
+provided if some form of flow analysis was performed before compilation.
+3.  The AI proposes that postconditions are evaluated at the end of a
+subprogram's normal execution but before any copying back of exported
+parameters.  Unfortunately, if the postcondition assertion fails, then
+any parameters passed by reference and updating global variables will
+already have been modified.  The system "state" is therefore in an
+unknown condition when the exception is raised making its use in
+deployed systems problematic.  The fact that system behaviour after a
+failed postcondition depends on the parameter passing mechanism used
+introduces a new and unwelcome form of "undefined" behaviour which is
+inappropriate for the high-integrity systems at which the AI is aimed.
+4.  The proposed freedom to allow any form of pre and postcondition for
+overidden tagged operations is dangerously flawed.  For any sensible
+tagged type hierarchy, it must be the case that:
+Root op precondition        -> Overridden op precondition and
+Overridden op postcondition -> Root op postcondition.
+In other words, an overriding operation must "ask less and promise
+more".  These rules are well established by the work of  Barbara Liskov
+and Jeannette Wing and are partially implemented in Eiffel.  Any attempt
+to present Ada as providing "programming by contract" which was even
+weaker than Eiffel in this respect would be very harmful to the
+credibility of the language.
+The HRG cannot support this proposal in its current form.
+From: Tucker Taft
+Sent: Tuesday, January 7, 2003,  6:00 AM
+Well, that is a "pan" if I ever saw one ;-).
+However, I am wondering whether the HRG had any notion
+of what "form" of proposal they might support?
+... or do they conclude that any improvement in this area
+is beyond the scope of the standard?  In other words,
+was the ultimate suggestion "drop it" or "try harder"?
+From: Alan Burns
+Sent: Tuesday, January 7, 2003,  7:21 AM
+In such stark terms I think the view was "drop it", but let me
+deconstruct that a bit. The HRG looked at these as `do they
+help verification', in other words do they help static analysis.
+And the view was no they do not (for reasons explained in the
+emails). But if you view these AIs as helping construct run-time
+checks for protected execution then they may well be fine.
+The HRG does not believe that the static analysis and dynamic protection
+can be obtained from the same language primitives. Static analysis
+needs so much extra stuff (specifications, visibility into inner
+scopes etc) if these are represented as comments then there is no
+confusion. Run-time checks are part of the execution and have a
+different role.
+So do not drop it if there is value in terms of dynamic protection,
+just put the emphasis there.

Questions? Ask the ACAA Technical Agent