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: fac41,2c6139ce13be9980
X-Google-Attributes: gidfac41,public
X-Google-Thread: f43e6,2c6139ce13be9980
X-Google-Attributes: gidf43e6,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.872044276@merv>#1/1
X-Deja-AN: 265433670
References: <5siqrr$3of@jupiter.milkyway.org>
 <5smgts$p68$1@miranda.gmrc.gecm.com> <33EFCCE4.4CE0@flash.net>
 <5sq3fh$frg@wdl1.wdl.lmco.com> <dewar.871993443@merv>
 <33F9C7BD.794BDF32@eiffel.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>


Bertrand says

<<You obviously must know better. The postcondition, if it
needs to be expressed, is something like "string XXX" [the
argument to the routine] "has been appended to the output".
With the proper model this is easy to express formally.>>

But that's the whole point. Sure you can write a (pretty useless)
postcondition after 

print ("this is my useless error message");

to make sure you have added that string to the output file, but that tests
only whether your code is working, not whether it meets the specification,
which was to produce intelligible error messages. And I do not know what
you mean by "know better". If you mean do I know perfectly well that
postconditions cannot capture this kind of specification, yes, I know
that perfectly well -- many specifications and requirements cannot be
formalized in any useful manner.