Type declarations on method parameters and return values are also constraints on the possible values that can be passed between a method and its caller. As such, they form part of the contract for the method. This is, in fact, a required part of the contract in statically-typed languages. (Unfortunately, this is typically the only part of the contract that gets written.)
Suppose you have a class called Complex representing complex numbers, and a method that adds two numbers and returns the result. In an object-oriented fashion, the method signature will be Complex add(Complex other), and a call c1.add(c2) will add the numbers c1 and c2 and return the sum. The type declaration "Complex other" in the method signature is a precondition that requires callers to pass only objects of type Complex to this method, and the declaration that the result is Complex is a postcondition ensuring that only Complex objects will ever be returned by the method.
Normally, we don't really think of type declarations as a contract, since they are enforced by the compiler and no further action is required by the programmer to ensure that the contracts are indeed satisfied. But if you think of type declarations as contracts in the context of Liskov's Behavioral Subtyping Principle, they have interesting consequences. One is that subclasses are only allowed to strengthen postcondition but never weaken them. This means that subclasses may return more specialized types than Complex. This is not surprising; it is quite likely that there are several implementations of complex number, all of which are subtypes of Complex; for example, ComplexAsCartesian and ComplexAsPolar, referring to the two most common representations of complex numbers. It is perfectly permissible for the add method of each subclass to return elements of that subclass (although that is not always the best policy). But can you redefine the return type of ComplexAsCartesian.add to be ComplexAsCartesian rather than just Complex as in the superclass? The answer depends on the programming language, and even on the language version. For example, Java originally didn't allow any changes in method signatures, but since Java 5 it is possible to redeclare more specific types (that is, subtypes) for method return values.
This kind of change, where subclasses use subtypes of those used in their superclasses, is called a covariant change, since the direction of change is the same: as you go down the inheritance hierarchy, types get more specialized (that is, also go down). Covariance is very natural to use in practice. In addition to the example above, you can think of modeling artifacts (physical or virtual) that need to be connected in various ways. Often, as you become more specific in one dimension, you need to be more specific in others. For example, every laptop needs a power supply. But specific laptops have dedicated power supplies, and you can't use any power supply with any laptop. So the most abstract Laptop class may define an attribute called powerSupply, whose type is PowerSupply. But an ABCLaptop requires an XYZPowerSupply, so the type of the power supply goes down the hierarchy as the type of the laptop goes down.
Covariance is all very well for method return types, where it fits the Behavioral Subtyping Principle. But it contradicts the principle for method arguments. The type of a method argument is like a precondition, since it constrains the values that the caller can pass to the method. Preconditions may only be weakened in subtypes; this means that argument types can only be generalized in subtypes. This is called contravariance, since argument types to up the hierarchy in subtypes. So here we have a conflict between what is theoretically correct (contravariance for argument types) and what is useful (covariance).
There is a large debate on this issue, and different languages treat it differently. None of C/C++, Java, or C# allow any change in argument types (this is called invariance). This is, in fact, unrelated to the issue of covariance versus contravariance; it is a consequence of the fact that these languages support overloading (see Overriding and Overloading). As a result, any change in method argument types defines an overloaded method, which is unrelated to the original method. Eiffel follows the practical route, supporting covariance of argument types, and incurring the inevitable cost. This cost is the lack of compile-time type checking for these cases. In statically-typed languages, including all the ones mentioned above, we expect the compiler to type-check the program so that no type violations will occur at runtime (with some other notable exceptions, such as type casting and some uses of generics in Java). Covariance creates another exception to this rule.
Of course, preventing covariance in the language doesn't solve anything, since in practice it is still necessary. What programmers do when the language doesn't support covariance is to write their own tests in subclasses, checking for the correct subtypes and throwing exceptions when they are incorrect. So even though the program is fully type-checked, there are still type-related exceptions at runtime. But because these are programmed manually rather than being thrown by the language runtime, language designers feel it isn't their responsibility. This ostrich effect is, of course, completely pointless.
Showing posts with label Logic. Show all posts
Showing posts with label Logic. Show all posts
Sunday, May 22, 2011
Thursday, May 5, 2011
Abstract Preconditions
Returning to the example of the Set type, suppose now that its implementation ArraySet uses a fixed-size array to hold the set elements, and is therefore limited in size (or "bounded"). The maximum size, called the set's capacity, is given when the ArraySet object is constructed and the array is allocated. The method ArraySet.add, which can add a new element to the set, now needs to have a postcondition size() < capacity(), where size() returns the current size of the set and capacity() returns the maximum size.
Side note: in such cases, it is common to provide the size() method, but less careful designers don't provide capacity(). The assumption is that you ought to know the capacity, since you gave this value when creating the set. But, of course, you may be using a set created by someone else. Writing contracts often alerts you to the necessity of adding such informative methods.
According to Liskov's Behavioral Subtyping Principle (see The Correct Use of Inheritance), ArraySet may not strengthen a method precondition. Therefore, Set must also declare the same precondition (or a stronger one) on the add method. In general, however, sets don't need to be bounded, and therefore this precondition is inappropriate there. What is wrong? The first thing to question is the inheritance hierarchy: is ArraySet really a subtype of Set? More generally, are bounded sets types of sets? At first blush, the answer is obviously yes. But on deeper thought, it seems that we have our abstractions a little bit off. There are really three concepts involved here: general sets, bounded sets, and unbounded sets. Both bounded and unbounded sets are kinds of sets; bounded sets have the size() < capacity() precondition, while unbounded sets don't. Again, it seems like general sets must have this precondition as well, to comply with the Behavioral Subtyping Principle.
Certainly, general sets need to have some precondition that subsumes the boundedness condition, but it doesn't need to have the same form. The abstract meaning of the precondition is that the set may not be full when adding a new element. In this form, the precondition is applicable to any set; bounded sets may sometimes be full, while unbounded sets will never be full. So we need to add to the Set type, which represents general sets, a method full() that returns a boolean value. The precondition on Set.add will be !full(). At this level, this precondition is abstract: its precise meaning is unknown. A client that uses an object of this type therefore needs to check that the set isn't full before adding an element. The implementation of Set.full may provide some default value, or may be absent, in which case the Set type itself is abstract.
ArraySet.full overrides Set.full to return the value of the expression size() < capacity(). In addition, this method has a postcondition $ret == size() < capacity(). Clients of ArraySet now know the precise condition under which they are permitted to call the add method. In contrast, unbounded implementations of Set, such as HashSet, override Set.full() to return false, with a postcondition $ret == false (or !$ret). Clients of HashSet therefore know that the precondition on add is really vacuous: it will never be true, and therefore they are allowed to call add under all circumstances.
If the concepts of bounded and unbounded sets are deemed important enough, it is possible to define them as classes (or interfaces) in their own right, and put the relevant contracts there. In this way, the missing abstractions are crystallized in the design, with precise contracts that obey the Behavioral Subtyping Principle without forcing a formulation of the precondition that is specific to a subtype.
Side note: in such cases, it is common to provide the size() method, but less careful designers don't provide capacity(). The assumption is that you ought to know the capacity, since you gave this value when creating the set. But, of course, you may be using a set created by someone else. Writing contracts often alerts you to the necessity of adding such informative methods.
According to Liskov's Behavioral Subtyping Principle (see The Correct Use of Inheritance), ArraySet may not strengthen a method precondition. Therefore, Set must also declare the same precondition (or a stronger one) on the add method. In general, however, sets don't need to be bounded, and therefore this precondition is inappropriate there. What is wrong? The first thing to question is the inheritance hierarchy: is ArraySet really a subtype of Set? More generally, are bounded sets types of sets? At first blush, the answer is obviously yes. But on deeper thought, it seems that we have our abstractions a little bit off. There are really three concepts involved here: general sets, bounded sets, and unbounded sets. Both bounded and unbounded sets are kinds of sets; bounded sets have the size() < capacity() precondition, while unbounded sets don't. Again, it seems like general sets must have this precondition as well, to comply with the Behavioral Subtyping Principle.
Certainly, general sets need to have some precondition that subsumes the boundedness condition, but it doesn't need to have the same form. The abstract meaning of the precondition is that the set may not be full when adding a new element. In this form, the precondition is applicable to any set; bounded sets may sometimes be full, while unbounded sets will never be full. So we need to add to the Set type, which represents general sets, a method full() that returns a boolean value. The precondition on Set.add will be !full(). At this level, this precondition is abstract: its precise meaning is unknown. A client that uses an object of this type therefore needs to check that the set isn't full before adding an element. The implementation of Set.full may provide some default value, or may be absent, in which case the Set type itself is abstract.
ArraySet.full overrides Set.full to return the value of the expression size() < capacity(). In addition, this method has a postcondition $ret == size() < capacity(). Clients of ArraySet now know the precise condition under which they are permitted to call the add method. In contrast, unbounded implementations of Set, such as HashSet, override Set.full() to return false, with a postcondition $ret == false (or !$ret). Clients of HashSet therefore know that the precondition on add is really vacuous: it will never be true, and therefore they are allowed to call add under all circumstances.
If the concepts of bounded and unbounded sets are deemed important enough, it is possible to define them as classes (or interfaces) in their own right, and put the relevant contracts there. In this way, the missing abstractions are crystallized in the design, with precise contracts that obey the Behavioral Subtyping Principle without forcing a formulation of the precondition that is specific to a subtype.
Friday, April 15, 2011
Overriding and Overloading
Two terms that sound similar and are sometimes confused are overriding and overloading. The former is an essential part of inheritance, and therefore of object-oriented programming; the latter is a syntactic device that adds no expressive power to the language.
Overriding a method means providing a new implementation for it in an inheriting class. This may be necessary because the subclass has a different representation, which has more information than the superclass. For example, suppose you are programming an interactive game, in which characters lose health points as a result of exertion or by attacks by other players. This is implemented through a method damage(int points), which inflicts the given amount of damage. Now assume that you create a special kind of character, called Merlin, which can make itself invisible as well as operate a force shield that protects it from certain kinds of enemy actions. However, it can't perform these new functions when its health is too low. The class implementing the Merlin character inherits from the general character class. It needs to override the implementation of the damage method, in order to disable invisibility and the force shield if the health level drops below the relevant thresholds. When the damage method is called for any character, it decreases its health; for Merlin, it may additionally disable his special abilities.
The choice of which code runs for a particular invocation of the damage method is made at runtime. If the character happens to be Merlin (that is, its type is the Merlin class), the code executed will come from the Merlin class. If the character's type is another class, the code will be taken from that class, or from the closest ancestor class that provides an implementation of that method. This is called dynamic dispatch, and is a cornerstone of object-oriented programming.
Merlin's special abilities can be damaged by special types of attacks, which do not otherwise damage his overall health. It seems natural to add to Merlin's class a new method, damage(Ability ability), which damages the given ability but does not affect other abilities or the health measure. This is a case of overloading: using the same name for two different methods. Many, but not all, object-oriented languages support overloading. Java, C#, and C++ all do, while Eiffel doesn't. The choice of which code gets executed in a call to the overloaded damage method is made by the compiler: if the argument is an int, the general damage method will be called; if the argument is an Ability (that is, its type is the Ability class), the second will be called. These types must be known at compile time; if they aren't, the program won't compile.
Because the decision of which overloaded method to call is static, it is known to the programmer writing the call. Therefore, overloading can always be replaced by renaming methods. In our example, the new method that damages Merlin's special abilities can be called damageAbility to remove the overloading. In fact, overloaded methods are implemented using this technique; languages such as C++, Java, and C# have a special notion of method name, which attaches encoded information about argument types to the method name as defined by the programmer.
When used properly, overloading can make programs more understandable. For example, the + operator is overloaded in Java to represent addition of integers as well as floating-point numbers. That's perfectly understandable, since the mathematical addition operator applies to all these types and has the same properties for them (associativity, commutativity, etc.). It would be perfectly fine to use + for adding complex numbers if Java allowed this (and is common in C++, which does). However, Java overloads + to denote concatenation of strings as well. This is confusing, and is a design error of the language. This error is compouned by the fact that + coerces its arguments to more general types, so that x + y will denote floating-point addition if x is an int and y is a float, but string concatenation if x as an int and y is a string. Worse yet, mathematical properties of addition don't hold for string concatenation, and as a result ("a" + 1) + 2 is "a12" while "a" + (1 + 2) is "a3".
Because overloading doesn't add to the expressive power of the language, and is a trap for the unwary, it should be removed from object-oriented languages. Unfortunately, the C++/Java/C# family of languages encourage overloading, and even require it in the case of constructors, whose names must be the name of the class. Suppose you want to create a complex-number class called Complex, and give it two constructors, one receiving the rectangular representation of the number (x and y for x+iy) while the other receives the polar representation (rho and theta for rho*e^(i*theta)). You want to call these two constructors by descriptive names, such as complexFromRectangular and complexFromPolar. But in C++/Java/C#, both must be called Complex! Not only are the names non-descriptive, they also coincide, because both constructors take two arguments of the same types. I won't describe the contortions that programmers of these languages have to go through to solve this problem.
My recommendation: avoid overloading altogether. If you really feel it's essential in some case, at least make sure that the overloaded methods have the same semantics (as in the case of mathematical addition). If you use overloading in other cases (such as addition and concatenation), you will have only yourself to blame when you get confused; and your users will be perfectly justified in blaming you when they, in turn, get confused.
Overriding a method means providing a new implementation for it in an inheriting class. This may be necessary because the subclass has a different representation, which has more information than the superclass. For example, suppose you are programming an interactive game, in which characters lose health points as a result of exertion or by attacks by other players. This is implemented through a method damage(int points), which inflicts the given amount of damage. Now assume that you create a special kind of character, called Merlin, which can make itself invisible as well as operate a force shield that protects it from certain kinds of enemy actions. However, it can't perform these new functions when its health is too low. The class implementing the Merlin character inherits from the general character class. It needs to override the implementation of the damage method, in order to disable invisibility and the force shield if the health level drops below the relevant thresholds. When the damage method is called for any character, it decreases its health; for Merlin, it may additionally disable his special abilities.
The choice of which code runs for a particular invocation of the damage method is made at runtime. If the character happens to be Merlin (that is, its type is the Merlin class), the code executed will come from the Merlin class. If the character's type is another class, the code will be taken from that class, or from the closest ancestor class that provides an implementation of that method. This is called dynamic dispatch, and is a cornerstone of object-oriented programming.
Merlin's special abilities can be damaged by special types of attacks, which do not otherwise damage his overall health. It seems natural to add to Merlin's class a new method, damage(Ability ability), which damages the given ability but does not affect other abilities or the health measure. This is a case of overloading: using the same name for two different methods. Many, but not all, object-oriented languages support overloading. Java, C#, and C++ all do, while Eiffel doesn't. The choice of which code gets executed in a call to the overloaded damage method is made by the compiler: if the argument is an int, the general damage method will be called; if the argument is an Ability (that is, its type is the Ability class), the second will be called. These types must be known at compile time; if they aren't, the program won't compile.
Because the decision of which overloaded method to call is static, it is known to the programmer writing the call. Therefore, overloading can always be replaced by renaming methods. In our example, the new method that damages Merlin's special abilities can be called damageAbility to remove the overloading. In fact, overloaded methods are implemented using this technique; languages such as C++, Java, and C# have a special notion of method name, which attaches encoded information about argument types to the method name as defined by the programmer.
When used properly, overloading can make programs more understandable. For example, the + operator is overloaded in Java to represent addition of integers as well as floating-point numbers. That's perfectly understandable, since the mathematical addition operator applies to all these types and has the same properties for them (associativity, commutativity, etc.). It would be perfectly fine to use + for adding complex numbers if Java allowed this (and is common in C++, which does). However, Java overloads + to denote concatenation of strings as well. This is confusing, and is a design error of the language. This error is compouned by the fact that + coerces its arguments to more general types, so that x + y will denote floating-point addition if x is an int and y is a float, but string concatenation if x as an int and y is a string. Worse yet, mathematical properties of addition don't hold for string concatenation, and as a result ("a" + 1) + 2 is "a12" while "a" + (1 + 2) is "a3".
Because overloading doesn't add to the expressive power of the language, and is a trap for the unwary, it should be removed from object-oriented languages. Unfortunately, the C++/Java/C# family of languages encourage overloading, and even require it in the case of constructors, whose names must be the name of the class. Suppose you want to create a complex-number class called Complex, and give it two constructors, one receiving the rectangular representation of the number (x and y for x+iy) while the other receives the polar representation (rho and theta for rho*e^(i*theta)). You want to call these two constructors by descriptive names, such as complexFromRectangular and complexFromPolar. But in C++/Java/C#, both must be called Complex! Not only are the names non-descriptive, they also coincide, because both constructors take two arguments of the same types. I won't describe the contortions that programmers of these languages have to go through to solve this problem.
My recommendation: avoid overloading altogether. If you really feel it's essential in some case, at least make sure that the overloaded methods have the same semantics (as in the case of mathematical addition). If you use overloading in other cases (such as addition and concatenation), you will have only yourself to blame when you get confused; and your users will be perfectly justified in blaming you when they, in turn, get confused.
Friday, April 8, 2011
Writing Contracts
In the best thriller tradition, we left our hero, the Set type, in an awkward position at the end of the last episode. Because Set has a subtype, HashSet, that doesn't allow nulls as values, the method Set.add(Object x) needed to have a precondition x != null. But Set has another subtype, ArraySet, which does allow null values. Therefore, we couldn't put a postcondition on Set.get() that guarantees that the returned value won't be null. The Set type now precludes null inputs, but may return null values; this seems inconsistent. Yet both contract decisions seem to be forced by Liskov's Behavioral Subtyping Principle!
In such cases, it is often helpful to look for missing abstractions. Here, there is an obvious correlation between null inputs and outputs: some sets support null values in both cases, and the others don't in either. The Set type should clearly distinguish between the two types of sets, by means of a query such as supportsNullValues(). The precondition of Set.add(Object x) will now be:
!supportsNullValues() ==> x != null
where "==>" denotes logical implication. The postcondition of Set.get() will be:
!supportsNullValues() ==> $ret != null
where "$ret" denotes the returned value. The contract for Set is now consistent in both cases. If supportsNullValues() is true, the precondition on add and postcondition on get are inactive; if it's false, both are active.
Furthermore, we can now add a postcondition to HashSet.supportsNullValues(): $ret == false (or, equivalently, !$ret). As a result, developers using HashSet know, by examining the contract, that add must not be given null values and get will never return null. Similarly, ArraySet.supportsNullValues() will have a postcondition $ret == true (or simply $ret). Developers using ArraySet will now know that they can provide add with null inputs, and may receive nulls from get. Developers who use the Set type without knowing the particular implementation can act in one of two ways. First, they can be cautious and not insert any null values into the set. Because Set.get will only return elements previously inserted into the set, it won't return null in this case. (Note that this is part of the contract that is difficult to specify formally, since it involves conditions on the behavior of the set over time. However, it is an important part of the contract, and should be documented as such, using natural language.) The second option is to call supportsNullValues() and act according to the value returned.
In the example, Set.add had another precondition that stated that the client is not allowed to add to the set an element that is already in it. This is legal but not recommended. In general, preconditions should contain any conditions under which the action of the method is not well defined. For example, it makes no sense to ask for an element of an empty set, which is why Set.get has a precondition that the set isn't empty. But adding to the set an element that is already there is perfectly well defined; the set simply doesn't change. Instead of requiring clients to check this condition before calling add, the implementation of the add method should simply do the right thing and not add the element if it already exists in the set. A little effort on the part of the implementer can save much effort for clients.
In such cases, it is often helpful to look for missing abstractions. Here, there is an obvious correlation between null inputs and outputs: some sets support null values in both cases, and the others don't in either. The Set type should clearly distinguish between the two types of sets, by means of a query such as supportsNullValues(). The precondition of Set.add(Object x) will now be:
!supportsNullValues() ==> x != null
where "==>" denotes logical implication. The postcondition of Set.get() will be:
!supportsNullValues() ==> $ret != null
where "$ret" denotes the returned value. The contract for Set is now consistent in both cases. If supportsNullValues() is true, the precondition on add and postcondition on get are inactive; if it's false, both are active.
Furthermore, we can now add a postcondition to HashSet.supportsNullValues(): $ret == false (or, equivalently, !$ret). As a result, developers using HashSet know, by examining the contract, that add must not be given null values and get will never return null. Similarly, ArraySet.supportsNullValues() will have a postcondition $ret == true (or simply $ret). Developers using ArraySet will now know that they can provide add with null inputs, and may receive nulls from get. Developers who use the Set type without knowing the particular implementation can act in one of two ways. First, they can be cautious and not insert any null values into the set. Because Set.get will only return elements previously inserted into the set, it won't return null in this case. (Note that this is part of the contract that is difficult to specify formally, since it involves conditions on the behavior of the set over time. However, it is an important part of the contract, and should be documented as such, using natural language.) The second option is to call supportsNullValues() and act according to the value returned.
In the example, Set.add had another precondition that stated that the client is not allowed to add to the set an element that is already in it. This is legal but not recommended. In general, preconditions should contain any conditions under which the action of the method is not well defined. For example, it makes no sense to ask for an element of an empty set, which is why Set.get has a precondition that the set isn't empty. But adding to the set an element that is already there is perfectly well defined; the set simply doesn't change. Instead of requiring clients to check this condition before calling add, the implementation of the add method should simply do the right thing and not add the element if it already exists in the set. A little effort on the part of the implementer can save much effort for clients.
Friday, April 1, 2011
The Correct Use of Inheritance
Perhaps the most subtle relationship in object-oriented programming is that of inheritance. Many object-oriented languages, including Java, distinguish between classes and interfaces, as a reaction to the problems languages such as C++ faced with multiple inheritance. This is a complex issue I will address in a later post. Now I want to focus on the logical relationships involved in inheritance. In order to avoid the class/interface dichotomy, I will use the notion of a subtype. A type A is a subtype of B if it inherits from it, whether both A and B are classes, both are interfaces, or A is a class and B is an interface. (Java uses the verb "extends" for the first two cases and "implements" for the third.)
An element of a subtype A may be used whenever an element of the supertype B is indicated. For example, suppose we have a type called Set that represents mathematical sets. It has a number of implementations inheriting from it, including ArraySet, which holds the elements of the set in an array, and HashSet, which holds the elements in a hash table. The Set type has various methods, including add(Object x), which adds an element to the set; get(), which returns an arbitrary element of the set; and has(Object x), which returns true if and only if x is in the set. Since a set can't contain the same object multiple times, we put a precondition on add(Object x) requiring that x is not already in the set: !has(x).
Unfortunately, our HashSet implementation doesn't support null as an element in the hash table, so we add another precondition to add(Object x), stating that x can't be null: x != null. Now, suppose we have a client C that uses our code, and receives a parameter s of type Set. When the programmer of the client code reads the contract for Set, he sees only one precondition: !has(x). He will certainly be careful not to insert the same element twice, for example by using the following code:
if (!s.has(element)) s.add(element);
But he has perfect confidence in the following piece of code:
if (!s.has(null)) s.add(null);
He will be rudely surprised, therefore, when this actually bombs on him somewhere inside the call to add in our HashSet implementation. He may not even have known about the existence of HashSet, since he received the object s, which happened to have this type, as a parameter. He is the proverbial innocent bystander, and should be protected from this kind of problem. After all, he kept his side of the contract, and has every right to expect us to keep our side!
This demonstrates a general problem, which will manifest itself whenever the precondition of a method in a subtype is stronger (that is, requires more) than that of the supertype. The rule must therefore be that subtypes are not allowed to strengthen method preconditions. We will have to add a precondition to Set.add, to warn potential users that some subtypes may not accept null as a parameter. Our ArraySet implementation can now weaken the precondition by removing this requirement. This is perfectly legal; clients that use ArraySet objects through the Set supertype will not be allowed to call add(null), but clients that use ArraySet directly will be able to enjoy the extended functionality.
Since we restrict Set.add not to accept null parameters, it looks like we can now put a postcondition on Set.get, stating that it will never return null. This will work well for HashSet, but will fail for ArraySet, which does accept null elements. By adding this postcondition to Set.get, we have again harmed innocent bystanders; in this case, a client of Set who happens to receive a HashSet object as its own parameter. Such a client feels perfectly justified in writing the following code:
if (!s.isEmpty()) System.out.println(s.get().toString());
He is careful to check the precondition of get, which states that it can't be called when the set is empty, and he is therefore entitled to rely on get's postcondition and to expect that no NullPointerException will be raised on the call to toString. He may not even be aware of the existence of ArraySet, and of the fact that it doesn't have this postcondition. The rule for postconditions therefore must be that postconditions must not be weakened by subtypes, although they can be strengthened; this enables clients of the subtype to benefit from extra features it supports.
These rules are consequences of Liskov's Behavioral Substitution Principle, which states that properties of the supertype must still be true of subtypes. This principle is true of all inheritance hierarchies which allow subtypes to be used as elements of their supertypes. After all, this is what a subtype means: if A is a subtype of B then every instance of A is, by definition, also an instance of B. (This does not apply to private inheritance in C++, which doesn't imply a subtype relationship, but it does apply to public inheritance in C++, as well as to all inheritance relationships in Java, C#, and similar languages.) The principle is true whether or not the developer uses design by contract, and writes contracts explicilty; a violation of the principle is still a bug, and a nasty one at that. Using design by contract makes it easier to prevent such violations in the first place.
Any developer who is ignorant of Liskov's Behavioral Substitution Principle can't claim to understand object-oriented programming, and should be prevented from writing any kind of inheritance relationship!
An element of a subtype A may be used whenever an element of the supertype B is indicated. For example, suppose we have a type called Set that represents mathematical sets. It has a number of implementations inheriting from it, including ArraySet, which holds the elements of the set in an array, and HashSet, which holds the elements in a hash table. The Set type has various methods, including add(Object x), which adds an element to the set; get(), which returns an arbitrary element of the set; and has(Object x), which returns true if and only if x is in the set. Since a set can't contain the same object multiple times, we put a precondition on add(Object x) requiring that x is not already in the set: !has(x).
Unfortunately, our HashSet implementation doesn't support null as an element in the hash table, so we add another precondition to add(Object x), stating that x can't be null: x != null. Now, suppose we have a client C that uses our code, and receives a parameter s of type Set. When the programmer of the client code reads the contract for Set, he sees only one precondition: !has(x). He will certainly be careful not to insert the same element twice, for example by using the following code:
if (!s.has(element)) s.add(element);
But he has perfect confidence in the following piece of code:
if (!s.has(null)) s.add(null);
He will be rudely surprised, therefore, when this actually bombs on him somewhere inside the call to add in our HashSet implementation. He may not even have known about the existence of HashSet, since he received the object s, which happened to have this type, as a parameter. He is the proverbial innocent bystander, and should be protected from this kind of problem. After all, he kept his side of the contract, and has every right to expect us to keep our side!
This demonstrates a general problem, which will manifest itself whenever the precondition of a method in a subtype is stronger (that is, requires more) than that of the supertype. The rule must therefore be that subtypes are not allowed to strengthen method preconditions. We will have to add a precondition to Set.add, to warn potential users that some subtypes may not accept null as a parameter. Our ArraySet implementation can now weaken the precondition by removing this requirement. This is perfectly legal; clients that use ArraySet objects through the Set supertype will not be allowed to call add(null), but clients that use ArraySet directly will be able to enjoy the extended functionality.
Since we restrict Set.add not to accept null parameters, it looks like we can now put a postcondition on Set.get, stating that it will never return null. This will work well for HashSet, but will fail for ArraySet, which does accept null elements. By adding this postcondition to Set.get, we have again harmed innocent bystanders; in this case, a client of Set who happens to receive a HashSet object as its own parameter. Such a client feels perfectly justified in writing the following code:
if (!s.isEmpty()) System.out.println(s.get().toString());
He is careful to check the precondition of get, which states that it can't be called when the set is empty, and he is therefore entitled to rely on get's postcondition and to expect that no NullPointerException will be raised on the call to toString. He may not even be aware of the existence of ArraySet, and of the fact that it doesn't have this postcondition. The rule for postconditions therefore must be that postconditions must not be weakened by subtypes, although they can be strengthened; this enables clients of the subtype to benefit from extra features it supports.
These rules are consequences of Liskov's Behavioral Substitution Principle, which states that properties of the supertype must still be true of subtypes. This principle is true of all inheritance hierarchies which allow subtypes to be used as elements of their supertypes. After all, this is what a subtype means: if A is a subtype of B then every instance of A is, by definition, also an instance of B. (This does not apply to private inheritance in C++, which doesn't imply a subtype relationship, but it does apply to public inheritance in C++, as well as to all inheritance relationships in Java, C#, and similar languages.) The principle is true whether or not the developer uses design by contract, and writes contracts explicilty; a violation of the principle is still a bug, and a nasty one at that. Using design by contract makes it easier to prevent such violations in the first place.
Any developer who is ignorant of Liskov's Behavioral Substitution Principle can't claim to understand object-oriented programming, and should be prevented from writing any kind of inheritance relationship!
Tuesday, March 8, 2011
Object-Oriented Contracts
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!
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!
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.
Saturday, February 26, 2011
Design by Contract
As I mentioned before, the state of the art in logics of programs isn't yet capable of verifying large-scale programs, even with the best theorem provers currently available. As a result, the vast majority of programmers don't use any formal methods during software development, and the term "verification and validation" refers mainly to testing. What many people don't realize is that there is a middle way in using formal methods; it is possible to improve software quality by using limited but effective parts of the theory.
Design by Contract is a method of using assertions in object-oriented programs to specify their behavior. This importance of this specification is first and foremost methodological. The mere fact of writing these specifications and having them available in libraries focuses programmer attention to the correct use of program interfaces. Many errors stem from misunderstandings; a simple but common example is when the writer of a method assumes that a certain parameter may not be null, and omitting to check or handle the case of a null pointer, while the client of the method assumes that the method does something reasonable when given a null value. The contract defines precisely the responsibilities of the client and supplier; in particular, if the method doesn't handle null pointers, it must declare that fact in its contract. This contract is a formal part of the interface, and (unlike the source code) must be available to all programmers who use the method. They, in turn, must look at the contract and behave according to their responsibilities in it.
This simple process of writing the contract for suppliers and consulting it when writing clients can prevent many errors before they are even made. In order for this to work, the contract doesn't even need to be completely formal, as long as it is precise. And it has to be simple enough to be easily understood, otherwise it is worthless and may even cause damage. However, if developers take the trouble of writing formal contracts, they can be rewarded by more than methodological advantages. Indeed, if contracts are written using a formal notation, it is possible to create tools that give additional benefits.
First, it is possible (though by no means trivial) to write tools that check the contract at runtime. Many errors are time bombs waiting to happen. For example, storing a null value in a field of an object may by itself cause no harm. Only later, when the field is accessed under the assumption that it can't contain null, does the software present an error (in Java, it would be a NullPointerException, nicknamed NPE). The process of finding where in the program the original null value was assigned can be difficult and time consuming. A debugger is a useful tool, but it takes skill and time to use it to track such errors, because in many cases the method call that assigned the null value has already completed its execution and is no longer available on the stack to be examined by the debugger. A tool that checks contracts at runtime would alert the developer to the problem much earlier, thus speeding both discovery and fix of the problem.
Contracts also enable some level of verification. Instead of having to prove that the program as a whole has some desired properties, the method and class contracts provide "stepping stones" to a (partial) proof of correctness. If we can prove that all calls in the program satisfy the method of the called method, we will have increased our confidence in the correctness of the program. Because proving such properties is much easier than proving correctness of a whole program, tools such as theorem provers can be more effective there. While there aren't yet any commercial tools that do that, there is a lot of research on this topic, and I expect the benefits of automated theorem provers to become practical first in this limited arena.
One of the important advantages of design by contract is that it provides incremental benefits. Programmers can get immediate benefit from simple contracts, such as those having to do with null pointers. By adding more details to the contract, they can get more benefit. It isn't necessary (or even useful) to attempt a full specification in order to use this methodology.
Purists may scoff and say that this is not what logicians mean by verification, and is no better than testing. I would agree with the first part of this statement, but not with the second. Contracts are complementary to testing, and both are necessary. (I will have more to say about this in the future.) If you insist in full verification, meaning proofs of complete correctness, you will not bring practical value to software development for a very long time. Design by contract is a practical and useful methodology that should be employed by every software developer. I will discuss some of the reasons why this is not yet the case in a future post.
Design by Contract is a method of using assertions in object-oriented programs to specify their behavior. This importance of this specification is first and foremost methodological. The mere fact of writing these specifications and having them available in libraries focuses programmer attention to the correct use of program interfaces. Many errors stem from misunderstandings; a simple but common example is when the writer of a method assumes that a certain parameter may not be null, and omitting to check or handle the case of a null pointer, while the client of the method assumes that the method does something reasonable when given a null value. The contract defines precisely the responsibilities of the client and supplier; in particular, if the method doesn't handle null pointers, it must declare that fact in its contract. This contract is a formal part of the interface, and (unlike the source code) must be available to all programmers who use the method. They, in turn, must look at the contract and behave according to their responsibilities in it.
This simple process of writing the contract for suppliers and consulting it when writing clients can prevent many errors before they are even made. In order for this to work, the contract doesn't even need to be completely formal, as long as it is precise. And it has to be simple enough to be easily understood, otherwise it is worthless and may even cause damage. However, if developers take the trouble of writing formal contracts, they can be rewarded by more than methodological advantages. Indeed, if contracts are written using a formal notation, it is possible to create tools that give additional benefits.
First, it is possible (though by no means trivial) to write tools that check the contract at runtime. Many errors are time bombs waiting to happen. For example, storing a null value in a field of an object may by itself cause no harm. Only later, when the field is accessed under the assumption that it can't contain null, does the software present an error (in Java, it would be a NullPointerException, nicknamed NPE). The process of finding where in the program the original null value was assigned can be difficult and time consuming. A debugger is a useful tool, but it takes skill and time to use it to track such errors, because in many cases the method call that assigned the null value has already completed its execution and is no longer available on the stack to be examined by the debugger. A tool that checks contracts at runtime would alert the developer to the problem much earlier, thus speeding both discovery and fix of the problem.
Contracts also enable some level of verification. Instead of having to prove that the program as a whole has some desired properties, the method and class contracts provide "stepping stones" to a (partial) proof of correctness. If we can prove that all calls in the program satisfy the method of the called method, we will have increased our confidence in the correctness of the program. Because proving such properties is much easier than proving correctness of a whole program, tools such as theorem provers can be more effective there. While there aren't yet any commercial tools that do that, there is a lot of research on this topic, and I expect the benefits of automated theorem provers to become practical first in this limited arena.
One of the important advantages of design by contract is that it provides incremental benefits. Programmers can get immediate benefit from simple contracts, such as those having to do with null pointers. By adding more details to the contract, they can get more benefit. It isn't necessary (or even useful) to attempt a full specification in order to use this methodology.
Purists may scoff and say that this is not what logicians mean by verification, and is no better than testing. I would agree with the first part of this statement, but not with the second. Contracts are complementary to testing, and both are necessary. (I will have more to say about this in the future.) If you insist in full verification, meaning proofs of complete correctness, you will not bring practical value to software development for a very long time. Design by contract is a practical and useful methodology that should be employed by every software developer. I will discuss some of the reasons why this is not yet the case in a future post.
Thursday, February 24, 2011
Logics of Programs
From the early days of computers, it was obvious that programming is difficult and error-prone. The mathematical nature of computer programs leads to the obvious thought that the same methods used to make sure that mathematical theorems are correct can help ensure that programs are correct. This has led to a lot of research on logics for computer programs. There are many abstractions of programs, and correspondingly many logics that deal with them.
At the simplest level, it is possible to think of a program as being executed sequentially, instruction by instruction. This is almost never true; even the simplest processors typically interrupt the sequential flow to handle external events, such as pressing a key on a keyboard or control panel connected to the computer. However, if we trust the operating system to make a clean separation between such interrupt handlers and the running application, then it is possible to think at a higher level of abstraction of some applications as running sequentially. But many application are concurrent by nature, and these are the most difficult to get right. There are many examples of small programs with two parallel components that have subtle and hard-to-find bugs in them, and parallel or concurrent systems are notoriously hard to program.
Even the simple sequential model requires special mathematical treatment, because it has to represent the changing state of the computer. Every operation in a program changes the state of the machine in some way; otherwise, there would be no point in executing it. There are many types of changes: first, the location of the next instruction (the "program counter") changes, either to the next instruction in the sequence, or to a different place for instructions that change the flow of control. Some instructions change the contents of memory, registers, or various control bits (for example, one that records whether the previous comparison resulted in a zero value). High-level languages hide some of these details, but most (with the notable exception of functional and logic languages) still have the notion of changing state.
A logical model of programs with changing state must represent this state explicitly. If x is a variable in a program, the formula x=3 is meaningless with respect to a program, because it may true or false in different states of the computation of the same program. The logical model must have an explicit representation of states, and some syntactic way of referring to different states. One of the best known formalisms is called Hoare logic, after C. A. R. Hoare, Turing prize winner and famous, among other things, as the inventor of the quicksort algorithm.
Every formula in this logic is a Hoare triple of the form {P}A{Q}, where A is a (possibly partial) program and P and Q are logical statements about the variables of the program. This formula asserts that if P holds in the state just prior to the computation of A, and if this computation terminates, then Q will be true in the resulting state. For example, a (somewhat simplified) way of describing the effect of an assignment x := e in a program is by the formula {e = c} x := e {x = c}, where c is a constant. (Note the crucial difference between logical equality and assignment, so unfortunately blurred by languages from Fortran to Java that use "=" for assignment.) This formula asserts that if the value of the expression e in the state preceding the assignment is c, than the value of x after the assignment is also c.
As another example, consider how to prove that a certain formula holds for a conditional: {P} if C then A else B {Q}. If the condition C is true in the state before the computation, then the conditional will choose the subprogram A. In order for the desired formula to hold, it must be the case that if P and C are true before the computation, Q must be true afterwards (provided, as always, that the computation terminates). Formally, {P and C} A {Q} must be true. Similarly, {P and not C} B {Q} must hold to guarantee the desired result in the case where the condition C is initially false. And indeed, the desired formula follows from the latter two in Hoare logic.
As is the case for most logics of programs, the difficulty lies in reasoning about loops (and recursion). In order to prove a property of a loop using these logics, it is necessary to come up with a loop invariant. This is a property that always holds at the beginning of each iteration. In order to prove a property P following the loop, you prove that the invariant holds on entry to the loop, that it sustains itself across one iteration, and that if you exit the loop with the invariant holding, P must be true at that point.
This is very similar to a proof by induction; the first step is the base of the induction, and the second is the inductive step, in which you prove that if the invariant holds in the beginning of one iteration, it also holds on the beginning of the next one. As is the case with inductive proofs, coming up with a suitable invariant is difficult. Much of the work of automatic theorem provers (for mathematics as well as for logics of programs) is discovering the induction hypotheses or, equivalently, the loop invariants. (In fact, in one of my favorite theorem provers, ACL2, these are exactly the same.)
This kind of reasoning is very low-level, and it is impossible to use it to prove the correctness of a large program manually. Automated theorem provers are a great help, but the process is still difficult and time-consuming, and requires high skills in logic and the specific theorem prover. It is therefore limited to relatively small but safety-critical programs. Wide application of automatic theorem proving to large-scale programs seems to be far in the future. As a result, there is a chasm between the people developing logics of programs and associated theorem provers, and the general population of software developers, most of whom are not even aware of the existence of these methods and tools. But there is a middle way; I will discuss it in the next post.
At the simplest level, it is possible to think of a program as being executed sequentially, instruction by instruction. This is almost never true; even the simplest processors typically interrupt the sequential flow to handle external events, such as pressing a key on a keyboard or control panel connected to the computer. However, if we trust the operating system to make a clean separation between such interrupt handlers and the running application, then it is possible to think at a higher level of abstraction of some applications as running sequentially. But many application are concurrent by nature, and these are the most difficult to get right. There are many examples of small programs with two parallel components that have subtle and hard-to-find bugs in them, and parallel or concurrent systems are notoriously hard to program.
Even the simple sequential model requires special mathematical treatment, because it has to represent the changing state of the computer. Every operation in a program changes the state of the machine in some way; otherwise, there would be no point in executing it. There are many types of changes: first, the location of the next instruction (the "program counter") changes, either to the next instruction in the sequence, or to a different place for instructions that change the flow of control. Some instructions change the contents of memory, registers, or various control bits (for example, one that records whether the previous comparison resulted in a zero value). High-level languages hide some of these details, but most (with the notable exception of functional and logic languages) still have the notion of changing state.
A logical model of programs with changing state must represent this state explicitly. If x is a variable in a program, the formula x=3 is meaningless with respect to a program, because it may true or false in different states of the computation of the same program. The logical model must have an explicit representation of states, and some syntactic way of referring to different states. One of the best known formalisms is called Hoare logic, after C. A. R. Hoare, Turing prize winner and famous, among other things, as the inventor of the quicksort algorithm.
Every formula in this logic is a Hoare triple of the form {P}A{Q}, where A is a (possibly partial) program and P and Q are logical statements about the variables of the program. This formula asserts that if P holds in the state just prior to the computation of A, and if this computation terminates, then Q will be true in the resulting state. For example, a (somewhat simplified) way of describing the effect of an assignment x := e in a program is by the formula {e = c} x := e {x = c}, where c is a constant. (Note the crucial difference between logical equality and assignment, so unfortunately blurred by languages from Fortran to Java that use "=" for assignment.) This formula asserts that if the value of the expression e in the state preceding the assignment is c, than the value of x after the assignment is also c.
As another example, consider how to prove that a certain formula holds for a conditional: {P} if C then A else B {Q}. If the condition C is true in the state before the computation, then the conditional will choose the subprogram A. In order for the desired formula to hold, it must be the case that if P and C are true before the computation, Q must be true afterwards (provided, as always, that the computation terminates). Formally, {P and C} A {Q} must be true. Similarly, {P and not C} B {Q} must hold to guarantee the desired result in the case where the condition C is initially false. And indeed, the desired formula follows from the latter two in Hoare logic.
As is the case for most logics of programs, the difficulty lies in reasoning about loops (and recursion). In order to prove a property of a loop using these logics, it is necessary to come up with a loop invariant. This is a property that always holds at the beginning of each iteration. In order to prove a property P following the loop, you prove that the invariant holds on entry to the loop, that it sustains itself across one iteration, and that if you exit the loop with the invariant holding, P must be true at that point.
This is very similar to a proof by induction; the first step is the base of the induction, and the second is the inductive step, in which you prove that if the invariant holds in the beginning of one iteration, it also holds on the beginning of the next one. As is the case with inductive proofs, coming up with a suitable invariant is difficult. Much of the work of automatic theorem provers (for mathematics as well as for logics of programs) is discovering the induction hypotheses or, equivalently, the loop invariants. (In fact, in one of my favorite theorem provers, ACL2, these are exactly the same.)
This kind of reasoning is very low-level, and it is impossible to use it to prove the correctness of a large program manually. Automated theorem provers are a great help, but the process is still difficult and time-consuming, and requires high skills in logic and the specific theorem prover. It is therefore limited to relatively small but safety-critical programs. Wide application of automatic theorem proving to large-scale programs seems to be far in the future. As a result, there is a chasm between the people developing logics of programs and associated theorem provers, and the general population of software developers, most of whom are not even aware of the existence of these methods and tools. But there is a middle way; I will discuss it in the next post.
Tuesday, February 15, 2011
Thinking Formally
If there is no alternative to clear thinking about our programs, we should investigate what we can learn from the science of organized thought. Logic has a long history, with equal roots in philosophy and mathematics. In some sense, computer programs breath life into abstract logic and give logic the abilitiy to do real things. And, just like Pinocchio, they often misbehave!
One of the fundamental concerns of logic is the study of proofs: how can we convince ourselves in a precise and mechanical way of the truth of some claim. The desire to do so resulted from the need to distinguish between valid and invalid mathematical proofs, expressed using prose. Sometimes, hidden assumptions were not recognized, leading to faulty proofs. For example, consider the first axiomatic proof system, Euclidean geomerty, studied in middle school. It has five axioms, including the famous "parallel postulate". It is an amazing achievement, which is still an excellent example of how to reason formally, and was the source of many important advances in mathematics. But Euclidean geometry has many hidden assumptions, which are glossed over by the use of informal drawings. About 2200 years after Euclid, several mathematicians tried to completely formalize geometrical proofs. David Hilbert's axiomatization of geometry includes twenty axioms instead of Euclid's five. One of these states that between every two different points on a straight line there is a third point on the same line. This was so obvious to Euclid that he didn't even think to mention it in his list of axioms. But axioms are exactly those self-evident propositions on which the theory is based, and the proof isn't logically sound unless all these are stated explicitly.
Logic is closely tied with computation, although the connection was made explicit only towards the 20th century. A formal proof is a series of deductions, each of which is based on axioms or previously-proven propositions, using a set of deduction rules. It is supposed to be so simple that it can easily be checked for correctness, without any understanding of its subject matter, whether it is geometry, number theory, or abstract algebra. In other words, it should be easy to write a program that checks a formal proof; all you need to do is verify that each step follows from the axioms and from previous steps according to the rules.
But wait! Is there a limit to the complexity of the axioms or of the rules used in the proof? Without such limits, the whole exercise falls apart. For example, imagine a system of axioms that contains all true statements in number theory. This is, of course, an infinite set. How difficult is it to write a program to check whether a given statement is an axiom? Well, it turns out to be impossible! (This is a consequence of Gödel's first incompleteness theorem.) So, if we are to be able to write a program to check formal proofs, we need to restrict the possible sets of axioms. For example, in Gödel's theorems, the set of axioms is required to be recursively enumerable; this means that there is a (finite) program that can generate all axioms and never generates anything that is not an axiom. Of course, this program will never terminate if the set is infinite. That's acceptable, as long as the program is guaranteed to produce every axiom if you wait long enough.
So now, a concept about computability has entered the study of logic itself. It is only fair, then, to apply logic to computation; and, indeed, the study of logics of programs is an important field in computer science. There are even computer programs called theorem provers, which have been used to prove difficult mathematical theorems as well as to verify the correctness of other programs. However, this has still not affected the day-to-day work of most software developers. In the next post, I will discuss why this is the case and what formal tools can still be used for software development today.
One of the fundamental concerns of logic is the study of proofs: how can we convince ourselves in a precise and mechanical way of the truth of some claim. The desire to do so resulted from the need to distinguish between valid and invalid mathematical proofs, expressed using prose. Sometimes, hidden assumptions were not recognized, leading to faulty proofs. For example, consider the first axiomatic proof system, Euclidean geomerty, studied in middle school. It has five axioms, including the famous "parallel postulate". It is an amazing achievement, which is still an excellent example of how to reason formally, and was the source of many important advances in mathematics. But Euclidean geometry has many hidden assumptions, which are glossed over by the use of informal drawings. About 2200 years after Euclid, several mathematicians tried to completely formalize geometrical proofs. David Hilbert's axiomatization of geometry includes twenty axioms instead of Euclid's five. One of these states that between every two different points on a straight line there is a third point on the same line. This was so obvious to Euclid that he didn't even think to mention it in his list of axioms. But axioms are exactly those self-evident propositions on which the theory is based, and the proof isn't logically sound unless all these are stated explicitly.
Logic is closely tied with computation, although the connection was made explicit only towards the 20th century. A formal proof is a series of deductions, each of which is based on axioms or previously-proven propositions, using a set of deduction rules. It is supposed to be so simple that it can easily be checked for correctness, without any understanding of its subject matter, whether it is geometry, number theory, or abstract algebra. In other words, it should be easy to write a program that checks a formal proof; all you need to do is verify that each step follows from the axioms and from previous steps according to the rules.
But wait! Is there a limit to the complexity of the axioms or of the rules used in the proof? Without such limits, the whole exercise falls apart. For example, imagine a system of axioms that contains all true statements in number theory. This is, of course, an infinite set. How difficult is it to write a program to check whether a given statement is an axiom? Well, it turns out to be impossible! (This is a consequence of Gödel's first incompleteness theorem.) So, if we are to be able to write a program to check formal proofs, we need to restrict the possible sets of axioms. For example, in Gödel's theorems, the set of axioms is required to be recursively enumerable; this means that there is a (finite) program that can generate all axioms and never generates anything that is not an axiom. Of course, this program will never terminate if the set is infinite. That's acceptable, as long as the program is guaranteed to produce every axiom if you wait long enough.
So now, a concept about computability has entered the study of logic itself. It is only fair, then, to apply logic to computation; and, indeed, the study of logics of programs is an important field in computer science. There are even computer programs called theorem provers, which have been used to prove difficult mathematical theorems as well as to verify the correctness of other programs. However, this has still not affected the day-to-day work of most software developers. In the next post, I will discuss why this is the case and what formal tools can still be used for software development today.
Subscribe to:
Posts (Atom)