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: 1108a1,2c6139ce13be9980 X-Google-Attributes: gid1108a1,public X-Google-Thread: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public From: dewar@merv.cs.nyu.edu (Robert Dewar) Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/08/24 Message-ID: #1/1 X-Deja-AN: 268347141 Organization: New York University Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-08-24T00:00:00+00:00 List-Id: Nick writes <<> OK, so if you can't write such requirements in a rigorous way, how can > you write the application. If you can write an application that meets > the requirements, you can write a coded spec for the problem. In the > extreme case, the code for the application is the specification.>> Many people have made statements like this, but in my experience, this is quite false. It is often the case that it is impossible to write down requirements in a rigorous way, either because you don't know what they are, or they are stated at a level of abstraction ("use a pleasing color scheme, easy on the eyes, for the GUI") that is not susceptible to formalization. Sure, the code for the application is *a* specification of *something*, but most likely it is *not* *the* desired specification. This is often frustrating to those who want a nice clean theoretical model that guarantees reliable code, but we need methods that can indeed handle the more general case where we do not always have rigorous specifications. Note that the problem of not being able to create such specifications is not restricted to hardware. Consider the two requirements that were placed on the IBM Trackpoint before its release: (a) On average, people must find it as easy to use out of the box as a trackball, even if they have experience with a trackball. (b) On average, people must find the trackpoint as easy to use as a mouse given extensive practice with both. These were taken very seriously, and the release of the product was delayed until these requirements were met. But I don't see how you could formalize these requirements into a form that would rigorously tell you if your mechanical device met these requirements. Once I heard Wirth state that one should simply refuse to attempt to write a program in such circumstances. His point was that it was impossible to guarantee correctness by the method he was proposing at the time (successive refinement, maintaining the invariant of correctness). My response (that what we needed was reliability, not correctness, and that correctness was only a tool to achieve reoliability), drew applause from the audience, which was frustrated by this narrow view. Things are not as simple as one might hope :-)