The most basic contract includes preconditions and postconditions for each modular unit (function, subroutine, method, or whatever it is called in a particular programming language). In object-oriented programming (OOP), there is an additional part of the contract, as well as interesting relationships between contracts in an inheritance hierarchy.
The basis of OOP is the association of operations with data types (or what are often called records in non-OO languages). Every object has a state, composed of the values of its fields (also called attributes). Operations on the object (often called methods) can access this state, and some also modify it. Every object represents some abstraction. These abstractions can be related to the application domain; for example, "employee", "salary", "student", "loan", or "flight segment". They can also be internal to the implementation; for example, "set of nodes visited in a graph", "queue of tasks to perform", or "database connection". It must always be possible to relate every concrete state of an object to the abstract entity it represents. The representation function takes a concrete state to the abstract object it represents.
In general, however, there may be possible object states that have no associated abstraction. For example, consider an implementation of a stack that uses an array rep to hold the objects in the stack together with an integer field count that represents the number of elements currently on the stack. If count is negative, the object represents no abstract object, since there is no stack with a negative number of elements. The representation function can therefore be partial: it isn't defined for all possible object states. It is important to give a precise characterization of the domain of the representation function, since this distinguishes meaningful object states from meaningless ones. If you ever find a meaningless object in your program, you know there's a bug in it. The characterization of the domain of the representation function as a logical formula is called the representation invariant; the word "invariant" signifies that this is a property that must be true for all objects at all times.
The third part of an object-oriented contract is therefore the class invariant. A crucial part of the class invariant is the representation invariant, but it can contain other assertions as well. The class invariant must be true for all objects of the class at all times except while a method of the class is executing. The last proviso is necessary since a method of the class may update several fields of the object; between the first and last updates, the object may be in an inconsistent state. This is unavoidable, but causes problems, especially with concurrent programs. Other problems arise from the fact that the invariant of one object may depend on other objects; for example, if an object that represents an agenda contains a list of items, each item must point back to the same agenda as its owner. This can be defined as an invariant of the agenda, but operations on the items may invalidate this property.
In simple cases, proving that the class invariant always holds (that is, it is really invariant) is similar to an inductive proof: you need to show that the invariant holds immediately following the construction of the object, and that it is maintained by every operation of the class. However, because of the problems mentioned above this isn't enough in many cases. Still, it is a necessary condition, and one that is often easy to check. Ignore it at your peril!
Tuesday, March 8, 2011
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.
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.
Subscribe to:
Posts (Atom)