Re: Assertions

[Richard D Riehle <laoXhai@ix.netcom.com>]

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