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: 1108a1,2c6139ce13be9980
X-Google-Attributes: gid1108a1,public
X-Google-Thread: f43e6,2c6139ce13be9980
X-Google-Attributes: gidf43e6,public
X-Google-Thread: 103376,3d3f20d31be1c33a
X-Google-Attributes: gid103376,public
From: leew@micrologic.com (Lee Webber)
Subject: Re: Safety-critical development in Ada and Eiffel
Date: 1997/08/20
Message-ID: <33faf0d7.732095@wizard.pn.com>#1/1
X-Deja-AN: 268284100
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> <dewar.872044276@merv>
Organization: Pioneer Global
Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel
Date: 1997-08-20T00:00:00+00:00
List-Id: <comp.lang.ada>


On 19 Aug 1997 22:33:04 -0400, dewar@merv.cs.nyu.edu (Robert Dewar)
wrote:

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

You've got a point here, but I think you're making too much of it.
This is a problem with all specification, not just assertions: you
can't formally specify an interface between a component of your system
and an external entity that itself is not specifiable.  But of course
everyone knows that.

This problem propagates all the way back to the requirements (how do
you engineer an "intelligible" set of messages so that they are
guaranteed to pass an acceptance test unless you specify the
acceptance test in advance?).  It isn't really an issue for the
solution domain.