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: 1108a1,5da92b52f6784b63 X-Google-Attributes: gid1108a1,public X-Google-Thread: ffc1e,a48e5b99425d742a X-Google-Attributes: gidffc1e,public X-Google-Thread: 107d55,a48e5b99425d742a X-Google-Attributes: gid107d55,public X-Google-Thread: f43e6,a48e5b99425d742a X-Google-Attributes: gidf43e6,public X-Google-Thread: 103376,a48e5b99425d742a X-Google-Attributes: gid103376,public X-Google-Thread: fac41,a48e5b99425d742a X-Google-Attributes: gidfac41,public From: jezequel@irisa.fr (Jean-Marc Jezequel) Subject: Re: Papers on the Ariane-5 crash and Design by Contract Date: 1997/03/18 Message-ID: <5gll90$2qu$1@news.irisa.fr>#1/1 X-Deja-AN: 226366560 Distribution: world References: <332B5495.167EB0E7@eiffel.com> <332D113B.4A64@calfp.co.uk> <5gl1f5$a26$2@quasar.dimensional.com> Organization: Irisa, Rennes (FR) Newsgroups: comp.lang.eiffel,comp.object,comp.software-eng,comp.programming.threads,comp.lang.ada,comp.lang.java.tech Date: 1997-03-18T00:00:00+00:00 List-Id: rkaiser@dimensional.com (Richard Kaiser): >>1) Documentation. You need less of this. Documentation which say 'This >>feature expects this and does that' is no longer need. Documentation >>that is needed is the 'intent' of the routine, and high level intent or >>overviews. There are tools that can produce what is called the short >>form, the code without the implementation built into most compilers. >>These will also produce HTML and other outputs. >The first mistake was to not put the time limit in some human readable >documentation, or if the time limit was documenting then it was not read. >Writing code so it documents itself reduces or eliminates the code >documentation, but this can be done in Ada, EIffel, C, C++ and even >assembly language and FORTRAN. These limits are part of the design >and belong in a Software Requirements/Requirements Verification document >and in the Version Description Document. And these documents must be >reviewed prior to reuse. Yes, that's the point!. And the interest of using Eiffel-like assertions is that there are standard tools (class abstracters) that are able to *automatically* extract this kind of document from the actual code, including *inherited* assertions. Assertions go farther than documenting the code: they document (parts of) the design. And because they are extracted from the code, they have more chances to stay up to date with the code itself. And clearly, the main interest of assertions (as design documentation) is to facilitate code review. Facilatating testing/debugging is only a side-effect, IMHO. >>4) Reviews. If you review code, then having the assertions in place >>is very useful. A large part of reviewing C++ is working out what >>assertions have been assumed, and checking code against them. Having >>them written into the code makes this easier. Imagine a Design by Contract approach applied to an Ariane5-like software system: - there is somewhere a function called convert (horizontal_bias) with a precondition horizontal_bias <= Maximum_bias - the function f that calls this function (convert(x)) must be sure that it is entitled to do it, that is that x <= Maximum_bias. If f cannot know, it means that there is a precondition of f of the form x <= Maximum_bias (the precondition is propagated to the caller). - idem for f' that calls f, and so on until either I know enough about the value of x, or eventually x comes from a source external to the package/module. In this last case, it means that the module has a precondition on an external reading. If you can prove that your external reading always respect the precondition (with some engineering margin) you're OK, as they were for Ariane4. If you try to reuse the module in another context, you're supposed to check its preconditions against the new environment. The saliant points of this approach are that: - it makes all assumptions in the code explicit at the level of a design document, automatically extracted from the code (and properly dealing with assertion inheritance issues) - coupled with a proper reviewing process (as it exist in this kind of mission-critical software), it allows the detection of this kind of problem early. To answer Jon S Anthony, yes, all that could have been done in Ada using: function Convert ( Horizontal_Bias: Integer ) return Integer is subtype Bias_Constraint is Integer range 0..Maximum_Bias; Require : Bias_Constraint := Horizontal_Bias; Ada's subtype declarations are a kind of contract, that could be documented as such. Design by contract is not specific to Eiffel. You can do it with any language, just because it is a way of designing! Eiffel is, however, one of the few languages that provide built-in support for it. Let's finally sum up what I perceive as the most important claims in this paper: - reusing a component without checking its full specification is dangerous, which means that simple minded CORBA-like approaches at building components for mission-critical software are doomed. - using design by contract is an interesting way to specify the behavior of a component - at least in the case of Ariane 501, simple assertions (a la Eiffel and other languages) would have been expressive enough to specify the fatal hidden assumption. Whether the last point scales up to a full sized mission critical system is still an open question. I'm quite confident it is so, but I've only my own experience with telco systems to back it up. -- Jean-Marc Jezequel Tel : +33 2 99847192 IRISA/CNRS Fax : +33 2 99847171 Campus de Beaulieu e-mail : jezequel@irisa.fr F-35042 RENNES (FRANCE) http://www.irisa.fr/pampa/PROF/jmj.html