Re: Papers on the Ariane-5 crash and Design by Contract

[rkaiser@dimensional.com (Richard Kaiser)]

In article <332D113B.4A64@calfp.co.uk>, Nick Leaton <nickle@calfp.co.uk> 
wrote:
>Path:
> dimensional.com!visi.com!news.maxwell.syr.edu!dispatch.news.demon.net!demon!ca
>lfp.demon.co.uk!not-for-mail
>From: Nick Leaton <nickle@calfp.co.uk>
>Newsgroups:
> comp.lang.eiffel,comp.object,comp.software-eng,comp.programming.threads,comp.l
>ang.ada,comp.lang.java.tech
>Subject: Re: Papers on the Ariane-5 crash and Design by Contract
>Date: Mon, 17 Mar 1997 09:39:07 +0000
>Message-ID: <332D113B.4A64@calfp.co.uk>
>References: <332B5495.167EB0E7@eiffel.com> <tz8ohcjv7cc.fsf@aimnet.com>
>NNTP-Posting-Host: calfp.demon.co.uk
>X-NNTP-Posting-Host: calfp.demon.co.uk
>X-Mailer: Mozilla 3.0Gold (X11; I; SunOS 5.5 sun4m)
>MIME-Version: 1.0
>To: Thomas <nouser@nohost.nodomain>
>Content-Type: text/plain; charset=us-ascii
>Content-Transfer-Encoding: 7bit
>Lines: 81
>Xref: dimensional.com comp.lang.eiffel:7803 comp.object:23425
> comp.software-eng:17269 comp.programming.threads:4199 comp.lang.ada:23371
> comp.lang.java.tech:8859
>Status: N
>
>Thomas wrote:
>
>> convert (horizontal_bias: INTEGER): INTEGER is
>>             require
>>                   horizontal_bias <= Maximum_bias
>>             do
>>                   ...
>> 
>>             ensure
>>                   ...
>> 
>>             end
>> 
>> What was required here was a simple check that a function argument was
>> within a certain range.  That check could have been expressed as an
>> Ada type declaration and checked by the compiler at compile time, or
>> as a runtime assertion/check.  The design team apparently decided that
>> either approach was too costly in terms of design or speed and instead
>> opted for leaving the code unsafe and documenting the conditions under
>> which the function could be used safely.  Also, they apparently did
>> not have a practice of annotating their code with assertion statements
>> for testing, and you suggest that they didn't have a standard
>> practice for documenting unchecked preconditions.
>> 
>> I don't see how the different notation that Eiffel uses for the same
>> purpose helps.  Eiffel's conditions are also enforced either at
>> compile time or at runtime, and exactly the same tradeoffs apply as
>> they do in the Ada program: you incur costs for type conversions and
>> range checks.  And if the programmer culture on a project is such that
>> they don't use Ada assertions, why would they use Eiffel
>> preconditions?
>> 
>
>Eiffel does type checking at compile time. You can check type at runtime
>but the need to do this is such that you should query if you write code
>that uses this feature. 
>
>        x ?= y
>
>x will be Void if y does not conform to they type of x.
>
>The point about culture and assertions is an interesting one. I have
>moved to a company that uses Eiffel. Initially I was very sceptical
>about assertions, for the same reason you are, that I don't see people
>using them, or that they remove them when the release the code.
>
>In practice though, you write them because as part of developing
>software they make a huge difference to development. This has an effect
>in various areas.
>
>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.

>2) Design. Writting assertions makes design easier. This is a personal
>observation and harder to justify. I find being clear about what
>something does helps clear up what I am doing. Having complex
>preconditions is not a good idea, again you probably don't have the
>right structure.

The code is going to say "I am not in my original application and may or
will fail?"  Assertions are only going to catch problems if there is:

>3) Debugging / Testing. Running with assertions enabled detects bugs 
>earlier. This is the real saver in time and costs. 

This is the

>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.
>
>There are other more complex parts to Eiffels assertion system, in
>relation to inheritance, and soon in relation to parallel processing.
>
>But in conclusion, my experience is that people write assertions in
>their code, because it is effective.
>
>