Interfacing contracts (Was: Eiffel and Java + Ada dispatching)

[geert@fozzie.sun3.iaf.nl (Geert Bosch)]

Joachim Durchholz (jhd@herold.franken.de) wrote:
  "This is the normal contract on parameter and result types. Eiffel  
   contracts also include arbitrary boolean expressions, extending the  
   contracting idea far into the area of program semantics.
   Just as a parameter type makes clear what sorts of parameters are  
   required, the preconditions make clear under what circumstances the  
   routine may be called and expected to return a correct result. The Eiffel  
   postconditions list what the routine guarantees to the caller in turn."

Although Ada's interface capabilities are good enough to define the
range of results, these extra capabilities of Eiffel are very useful indeed. 
Especially for the large programs that are built using Ada. 

Something I'd really like to have is an Ada extension for specifying
both interface constraints and implementation conditions. 

Example for interface specification that might be accepted by
an Ada implementation without violating the Ada-95 standard (yes?):

   --  Integer square root function truncating the exact result
   function Square_Root (I : Natural) return Natural;

   for Square_Root'Post_Condition use
      Square_Root (I)  ** 2 <= I and (Square_Root (I) + 1) ** 2 > I;

In implementation:
   function Square_Root (I : Natural) return Natural is
      Lowerbound : Natural := Natural'Min (2, I);
      for Lowerbound'Invariant use Lowerbound ** 2 <= I;
      ...
   begin
      ...
   end Square_Root;

The advantage of checkng the pre- and post-conditions is that
the user of the subprogram or primitive has a better specification
of what the function (or procedure or...) does. The advantage of
a machine checkable specification is that the user can rely on them.
Ordinary comments on the other hand are often out of date.

Also when my algorithm using the Square_Root function specified
above doesn't work correctly, I only have to look at the specification
to know that the error won't be in the Square_Root implementation.
This is much better than to try figuring out whether the Code is correct
or not. Using a pragma Assert on the computed value just before return
has some drawbacks: you have to look at the implementation to know whether
these assertions are present, and you have to make sure that all possible
returns from the function are checked.

Another point is that it is possible in many cases to automatically
prove invariants. When the proving software cannot prove invariants,
the programmer can (and maybe should) make smaller steps that are
easier to prove. When all invariants can be proved, no checks are
necessary so speed is the same.

Actually it might be possible for the compiler to take advantage of
invariants and pre- / post-conditions by both eliminating checks and
taking advantage of the extra information.
    
Note that in the examples above, the formal parameters are visible
in the expression and that the expression is in fact a function.

Regards,
   Geert
-- 
E-Mail: geert@sun3.iaf.nl