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=0.2 required=5.0 tests=BAYES_00,INVALID_MSGID, REPLYTO_WITHOUT_TO_CC 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: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public X-Google-Thread: fac41,2c6139ce13be9980 X-Google-Attributes: gidfac41,public X-Google-Thread: 1108a1,2c6139ce13be9980 X-Google-Attributes: gid1108a1,public From: donh@syd.csa.com.au (Don Harrison) Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/08/21 Message-ID: #1/1 X-Deja-AN: 265642638 Sender: news@syd.csa.com.au X-Nntp-Posting-Host: dev50 References: <33faf0d7.732095@wizard.pn.com> Organization: CSC Australia, Sydney Reply-To: donh@syd.csa.com.au Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-08-21T00:00:00+00:00 List-Id: Lee Webber wrote: :Robert Dewar wrote: : :>... 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: Exactly, and typically such requirements are both untestable yet obviously desirable (intelligible messages, for example). As a basic rule, if you can't specify something in verifiable terms, then it shouldn't be specified as a requirement. It should be recorded as desirable behaviour ("will" rather than "shall"): "Messages to the operator will be intelligible". Having said that, it's also true that verifiable specifications *do* get omitted from specifications, not because it's impossible to specify them, but because they're difficult to specify. Although some are unlikely to admit it, the Ariane profile thingo probably falls into that category. Don. =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Don Harrison donh@syd.csa.com.au