From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: f43e6,2c6139ce13be9980
X-Google-Attributes: gidf43e6,public
X-Google-Thread: fac41,2c6139ce13be9980
X-Google-Attributes: gidfac41,public
X-Google-Thread: 103376,3d3f20d31be1c33a
X-Google-Attributes: gid103376,public
X-Google-Thread: 1108a1,2c6139ce13be9980
X-Google-Attributes: gid1108a1,public
From: dewar@merv.cs.nyu.edu (Robert Dewar)
Subject: Re: Safety-critical development in Ada and Eiffel
Date: 1997/08/19
Message-ID: <dewar.871993443@merv>#1/1
X-Deja-AN: 265282451
References: <5siqrr$3of@jupiter.milkyway.org>
 <5smgts$p68$1@miranda.gmrc.gecm.com> <33EFCCE4.4CE0@flash.net>
 <5sq3fh$frg@wdl1.wdl.lmco.com>
Organization: New York University
Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel
Date: 1997-08-19T00:00:00+00:00
List-Id: <comp.lang.ada>


Mark says

<<Sure, even if assertions are required by the language syntax,
you can always just use the assertion "true" :-).
You can't even make using the assertion "true" illegal as there are
cases where the assertion "true" is exactly the correct assertion to
use; for example, using "true" as a precondition for a method documents the
fact that it has NO enviromential requirements at all. (E.G. a random
number routine or the Unix exit() call).  And, what is the postcondition
for printf()?>>

As for the last question, this is just the tip of the iceburg. Of course it
is not the case that all requirements can be caught by pre and post conditions.

The idea of using pre and post conditions and assertions is very old. It
is useful but by no means applicable in all cases.

What should be the post condition after outputting an error message
from a compiler?

pragma Assert (programmer now understands what they did wrong);

You need a *really* clever language to test that one (well I suppose the
assertion routine executed at runtime could ask the programmer whether
he understood :-)