Re: Assertions

["Nick Roberts" <nickroberts@callnetuk.com>]

Richard D Riehle wrote in message <7hqe7m$q7i@sjx-ixn1.ix.netcom.com>...
[...]
|    pragma Pre_condition  (boolean_expression [ ... ]);
|    pragma Post_condition (boolean_expression [ ... ]);


What would these actually do that Assert would not?

|    pragma Invariant      (boolean_expression [ ... ]);


This construct (I think) could be replaced by an Assert repeated in several
places.  Would it be so useful as to be worthwhile?  (Perhaps it would.)

|   with the further suggestion that we adopt Require, Ensure, and
|   Invariant from the Eiffel language.


For those of us Eiffel non-cognoscienti, what do these do, please?

|   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.

'Twas ever thus.  In all cases, the programmer must be as careful to put
something sensible into an Assert as into the code proper.

Assertions are certainly no panacea: sometimes the code to check up on a
piece of code would be more complex to write than the code it's checking;
sometimes there is no practical way to check up on it at all; M****y's L*w
ensures that bugs can get into the checking code as easily as they can get
into the code proper (and be just as much of a S*****g B****r to root out
;-).

|   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 would be grateful if you would expand a little on this, perhaps giving an
example or two.

I apologise to those who don't wish to retread this well-trodden ground, but
there some of us who missed the boat first time around, and need to retread
it.

-------------------------------------
Nick Roberts
-------------------------------------