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: f43e6,2c6139ce13be9980
X-Google-Attributes: gidf43e6,public
X-Google-Thread: 103376,3d3f20d31be1c33a
X-Google-Attributes: gid103376,public
From: WhiteR@no.spam.please.CRPL.Cedar-Rapids.lib.IA.US (Robert S. White)
Subject: Re: The stupidity of all the Ariane 5 analysts.
Date: 1997/07/23
Message-ID: <5r4952$nca$1@flood.weeg.uiowa.edu>#1/1
X-Deja-AN: 258283549
References: <33C835A5.362A@flash.net> <EDCo7K.Ezr@syd.csa.com.au>
 <33CC0548.4099@flash.net> <5qitoi$fdv$1@news.irisa.fr>
 <33CD6512.2404@flash.net> <01bc92e6$7a6f9e40$287b7b7a@tlo2>
 <33CEAF05.6389@flash.net> <33D2827B.41C67EA6@eiffel.com>
 <5qucs7$jie$3@flood.weeg.uiowa.edu> <33D3F2CB.61DC@flash.net>
Organization: If you have a good KTN then I might tell you.
Newsgroups: comp.software-eng,comp.lang.ada
Date: 1997-07-23T00:00:00+00:00
List-Id: <comp.lang.ada>


In article <33D3F2CB.61DC@flash.net>, kennieg@flash.net says...

>BTW, I just noticed the flaws in the example Eiffel code at the
>last minute (midnight Saturday, in fact). Did you and everyone
>else know it was wrong, and just not say anything, or did we
>all overlook the errors?


Do you mean what you addres in your Critique's paragraph 3.1.1 about
Meyer's Eiffel paper's solution code:

"...any software element that has such a fundamental constraint should 
state it explicitly, as part of a mechanism present in the programming 
language, as in the Eiffel construct

      convert (horizontal_bias: INTEGER): INTEGER is
            require
                  horizontal_bias <= Maximum_bias
            do
                  ...

            ensure
                  ...

            end

where the precondition states clearly and precisely what the input must 
satisfy to be acceptable."

  Yes it looks like the above code should do a floating point absolute
value on horizontal_bias before it checks against Maximum_bias.  But
I consider that a _typical_ coding error that is normally found by software
code inspections or unit level tests - whoops - DBC/Eiffel does _not_
find this error!  And yes, the test _must_ be done while the value is
still expressed in floating point _before_ conversion to integer...details,
details.  Stuff we encounter all of the time in our problem domain.

  One could argue that the above is just a nit (flawed example) and 
the overall premise of DBC/Eiffel as a "silver bullet" panacea versus
conventional "aerospace industry software engineering process" is 
the real issue.
_____________________________________________________________________
Robert S. White         -- An embedded systems software engineer
                  (newsgroups trimmed to contain the "language wars")