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,e01bd86884246855 X-Google-Attributes: gidfac41,public X-Google-Thread: 103376,fb1663c3ca80b502 X-Google-Attributes: gid103376,public From: Peter Amey Subject: Re: Interresting thread in comp.lang.eiffel Date: 2000/07/12 Message-ID: <396C24B1.F632039B@praxis-cs.co.uk>#1/1 X-Deja-AN: 645666286 Content-Transfer-Encoding: 7bit References: <8ipvnj$inc$1@wanadoo.fr> <8j67p8$afd$1@nnrp1.deja.com> <395886DA.CCE008D2@deepthought.com.au> <3958B07B.18A5BB8C@acm.com> <395A0ECA.940560D1@acm.com> <8jd4bb$na7$1@toralf.uib.no> <8jfabb$1d8$1@nnrp1.deja.com> <8jhq0m$30u5$1@toralf.uib.no> <8jt4j7$19hpk$1@ID-9852.news.cis.dfn.de> <3963CDDE.3E8FB644@earthlink.net> <3963DEBF.79C40BF1@eiffel.com> <396502D2.BD8A42E7@earthlink.net> <6aHa5.113$6E.23141@ptah.visi.com> <396B4A68.458FA3BC@maths.unine.ch> X-Accept-Language: en Content-Type: text/plain; charset=us-ascii X-Trace: 12 Jul 2000 08:57:42 GMT, 193.114.91.187 Organization: Praxis Critical Systems MIME-Version: 1.0 Newsgroups: comp.lang.ada,comp.lang.eiffel Date: 2000-07-12T00:00:00+00:00 List-Id: Ken Garlington wrote: > > "Bob Allen" wrote in message > news:u6hp4i16$GA.283@cpmsnbbsa07... > > > I hate reverting to overly simplistic examples, but I do not want to write > a > > book on > > this subject so here goes. > > > > Given the following methods of some math class, what is the semantics of > > each? > > REAL square_root(X:INTEGER) > > REAL inv(X:INTEGER) > > REAL tan(theta:REAL) > > > > square_root called with X = -1, what happens? > > exception, return a value indicating an error, return > > 0, -square_root(abs(X)), or somthing else > > Who should check if X < 0? > > for inv who checks for X = 0 > > is the result an exception or MAX_REAL > > for tan what happens if theta is a mutiple of 90+(180*n) or 270+(180*n) > > degrees? > Ken, you raise a number of very good points (as you have throughout this thread). Some of them, I think, indicate that contracts (regardless of whether contracts have any relevance to Ariane 5) are better enforced by proof than by language-defined executable constraints. Proof: 1. Has greater flexibility over _where_ you enforce the contract. 2. Requires no run time overhead for checking constraints. 3. Has no need for error handling code to deal with breeches of contract you have proved can't occur (and which will therefore turn out to be untestable). 4. Can express properties not directly visible according to the programming language rules at the point of check. (e.g. in SPARK we might define a proof function "NotFull(S : StackType) return Boolean;" which we can use for proof purposes even if the stack package does not export an Ada function which can tell us if the stack is full or not). For your square_root example we could say in SPARK: function square_root(X : Integer) return Integer; --# pre X >= 0; --this enforces a precondition proof check at each call --# return M => ( M * M = X ); --read as "return some M such that ..." Incidently, we can get the same precondition implicitly by simply making the parameter Natural instead of Integer (as we could use type Radians, Degrees or Mils to supply at least part of the contract for your Tan example). If we decided that the root operation had to be callable with any argument and was to return 0 for an invalid one we can remove the precondition and beef up the postcondition thus: function square_root(X : Integer) return Integer; -- no preconditon --# return M => ( X < 0 -> M = 0) and --# ( X >= 0 -> M * M = X ); This removes the obligation of the caller to check the value of X before making the call but, of course, may complicate what the caller can safely do with the returned value! Peter P.S. Apologies for those who have tried to look up SPARK on our web site in the last week - we are suffering the after effects of a lightning strike and it is still down (forgot to put "lighting_strike = false" in the precondition :-) -- --------------------------------------------------------------------------- __ Peter Amey, Product Manager ) Praxis Critical Systems Ltd / 20, Manvers Street, Bath, BA1 1PX / 0 Tel: +44 (0)1225 466991 (_/ Fax: +44 (0)1225 469006 http://www.praxis-cs.co.uk/ --------------------------------------------------------------------------