Thursday, March 3, 2011

What's in a Contract

The term "design by contract" is due to Bertrand Meyer, and is at the heart of his Eiffel language.  But the concept of using assertions to specify the behavior of small units of software (such as function calls) is much older, and not specific to the object-oriented paradigm.  Hoare logic, which I mentioned previously, consists of triples specifying program fragments with their preconditions and postconditions.  With objects, and especially with inheritance, come new features, but I want to start with simpler languages.

At the most basic level, the contract of a software unit (which I will refer to as a function) consists of a precondition and a postcondition.  The precondition is an assertion that must hold on entry to the function, and the postcondition must hold on exit.  Obviously, it is the caller's responsibility to ensure that the precondition is satisfied before making the call.  If that is not the case, then the function is under no obligation whatsoever; it may enter an infinite loop, return the wrong result, or blow up the computer.  In particular, it is not obliged to satisfy the postcondition.  However, if the precondition was true on entry, it is the supplier's responsibility to ensure that the computation of the function terminates, and that the postcondition holds on exit.

This scheme separates responsibilities very precisely between the client and supplier of the function, and enables modular reasoning.  As a simple example, suppose you need to use the sine function, and discover that the implementation you have has a precondition that the angle is between 0 and 90 degrees.  If the angle you want to compute the sine for happens to be in that range, you can go ahead and use the existing function.  If not, you can use elementary trigonometry to convert your angle to one that is between 0 and 90 degrees and has the same sine value, possibly with a different sign; in that case, you have to invert the sign yourself.  Of course, implementations of this function you are likely to encounter are able to compute the sine for any angle, and have no precondition.  It is, of course, crucial to know the difference between functions that have this precondition and those that don't.  If you call the former without being aware of the precondition, you are likely to get wrong results, which may or may not be easy to detect.

As another example, suppose you have a point (x, y) in the plain and you want to know the angle a line from the origin to (x, y) has with the positive direction of the x axis.  Mathematically, this is arctan(y/x).  However, the arctan function has a range of only 180 degrees; any implementation has to choose which range of values it will return.  Typical values might be –90 to 90 degrees, or 0 to 180.  This will be the correct angle only for two out of four quadrants in which the point (x, y) lies, and so you will need to convert the result to the proper quadrant based on the signs of x and y.  Here, you must know the postcondition of the arctan function, which will tell you what is the range of possible results.

If you have contracts for your function and those that it calls, you can now think of verifying that your implementation is correct.  You need to do is prove that your function fulfills its own contract, but instead of the proof having to involve all functions you call, and everything they call further down the chain, you only need to consider the contracts of called functions.  This is not necessarily easy, but it is much easier than having to consider all called code, which can be very large.  One thing you will still need to provide are loop invariants and variants for any loop in your own code.  (In Eiffel, these are part of the language, although they are not considered part of the contract.)

This leads to a modular proof style, in which each function can be verified separately.  Of course, you can only do full verification if contracts are complete specification.  But even if they aren't, you may still be able to prove important properties of your code.  Without contracts, this is a formidable task, which is very rarely even attempted.  It's a pity that many programmers are not aware of this possibility.

No comments:

Post a Comment