Re: Assertions

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

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