Re: Interresting thread in comp.lang.eiffel

[Peter Amey <pna@praxis-cs.co.uk>]

Ken Garlington wrote:
> 
> "Bob Allen" <ballen3@email.msn.com> 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/

--------------------------------------------------------------------------