In order to be able to deliver programs that exhibit correct behavior, we need to reason about them, so as to convince ourselves that the program will exhibit the correct behavior in all circumstances.
For example, consider the following program:
class Company {
String[] getLocations() {
return new String[] {"Brussels", "Paris", "Berlin"};
}
}
class Program {
static void printLocations(Company company) {
String[] locations = company.getLocations();
for (int i = 0; i < 3; i++)
System.out.println(locations[i]);
}
public static void main(String[] args) {
printLocations(new Company());
}
}
As part of reviewing this program to convince ourselves that it behaves correctly, we need to convince ourselves that the array accesses in method printLocations will never be out of bounds.
A straightforward approach to this reasoning task is to perform non-modular reasoning: to determine the behavior of a method call, we look inside the called method’s implementation. In the example, to determine the behavior of company.getLocations(), we look at the body of method getLocations() and see that it returns an array of length 3. From this observation, we can deduce that the array accesses in method printLocation will not fail.
This non-modular reasoning approach is brittle: if we convince ourselves of a program’s correctness through non-modular reasoning, and then change the implementation of any method anywhere in the program, we do not simply have to re-check the modified method; we also have to find all of the method’s callers, and re-check them as well. Indeed, the reasoning we used to convince ourselves of their correctness may have been invalidated by the modification. But it does not stop there: by the same argument, we have to re-check the callers’ callers as well, and so on. In fact, it’s even worse: since we may have taken context information into account when reviewing a method call, and the context may have changed due to the modification, we have to review not just the direct and indirect callers of the modified method, but all direct and indirect callees of the direct and indirect callers as well; that is, we effectively have to re-review the entire program.
For example, if we change method getLocations to return an array of size two, the reasoning we used to establish the correctness of method printLocations is invalidated. Indeed, executing method printLocations will now cause an out-of-bounds array access.
Does this mean that method printLocations is incorrect? Or does it mean that method getLocations is incorrect? The answer is: neither. With non-modular reasoning, there is no notion of correctness of methods; there is only the correctness of the program as a whole.
The solution, of course, is to perform modular reasoning instead. In the modular reasoning approach, we assign a specification to each method, which specifies the correct behaviors of the method. This way, we define a notion of correctness of a method: a method M is correct if and only if all of its behaviors are allowed by its specification, assuming that the method calls performed by M behave in accordance with the called methods’ specifications.
To convince ourselves of the correctness of a program, we simply need to check that each method complies with its specification, under the assumption that called methods comply with theirs. If each of a program’s methods is correct in this way, and the main method’s specification expresses the allowed behaviors of the program as a whole, then the correctness of the program as a whole follows as a corollary.
If we have verified a program modularly, and then we modify one of its methods, we only need to re-check that that one method still complies with its original specification. If so, we can immediately conclude that the correctness of the program as a whole is preserved.
If the changed method no longer complies with its original specification, we need to update its specification and re-verify its callers as well. This “change propagation” stops when we reach a method whose original specification is preserved.
In the example, there are at least two possible specifications that we can assign to method getLocations:
We can assign a strong specification:
/**
* @post | result != null
* @post | result.length == 3
* @post | Arrays.stream(result).allMatch(e -> e != null)
*/
String[] getLocations() {
return new String[] {"Brussels", "Paris", "Berlin"};
}
Given this specification for method getLocations, methods getLocations and printLocations are both correct. If we then change method getLocations
so that it returns an array of size two, the method no longer complies with
its specification so we need to update its specification and re-verify
callers as well. We will then discover that method printLocations needs to
be updated as well.
We can also assign a weaker specification:
/**
* @post | result != null
* @post | Arrays.stream(result).allMatch(e -> e != null)
*/
String[] getLocations() {
return new String[] {"Brussels", "Paris", "Berlin"};
}
Given this specification for method getLocations, method getLocations itself is correct but method printLocations is not correct. Indeed, from the specification of getLocations we cannot conclude that the array accesses performed by printLocations will not be out of bounds.
Suppose we update method printLocations as follows:
/** @pre | company != null */
static void printLocations(Company company) {
String[] locations = company.getLocations();
for (String location : locations)
System.out.println(location);
}
This modified version of printLocations is correct. Furthermore, suppose we now
change method getLocations to return an array of size two. This modified
version of getLocations still complies with its original specification, so we can conclude immediately that the correctness of the program as a whole is preserved. In particular, since during our review of method printLocations, we assumed only the specification of method getLocations and did not look at its implementation, the reasoning we used to conclude the correctness of method printLocations still holds, so we do not have to review method printLocations again.
Before we discuss modular reasoning about programs that use dynamic binding, we briefly review the concept of dynamic binding.
For each method call in a Java program, the Java compiler checks, before program execution starts, that there is a corresponding method in the program. It looks for this method by considering the static type of the target expression of the call (the expression before the dot) and the argument expressions. This process is known as method call resolution; we call the method found this way the resolved method.
Consider the following example program:
abstract class Company {
abstract String[] getLocations();
}
class CompanyA extends Company {
String[] getLocations() {
return new String[] {"Brussels", "Paris", "Berlin"};
}
}
class Program {
static void printLocations(Company company) {
String[] locations = company.getLocations();
for (int i = 0; i < 3; i++)
System.out.println(locations[i]);
}
public static void main(String[] args) {
printLocations(new CompanyA());
}
}
In this program, the resolved method of the call printLocations(new CompanyA()) in method main is the method printLocations in class Program. The static type of argument expression new CompanyA() is CompanyA, which is a subtype of the parameter type Company of the method. If the argument expression was "Hello" instead, method call resolution would fail, because String is not a subtype of Company.
Similarly, the resolved method of the call company.getLocations() in method printLocations is method getLocations in class Company, because the static type of target expression company is Company.
These two calls illustrate the two different types of method calls in Java:
printLocations(new CompanyA()) is a statically bound call: when the
call expression is evaluated at run time, the method called is exactly the
resolved method.company.getLocations() is a dynamically bound call.
When evaluating a dynamically bound method call expression,
the method called is either the resolved method or some method that
overrides it. More specifically, to determine which method is called,
the computer looks at the target object of the call, obtained by evaluating
the target expression:
if the class of the target object declares or inherits a method that
overrides the resolved method, then this method is called instead of the resolved method.
In the example program, when evaluating call expression
company.getLocations(), the target object is an object of class CompanyA (because main calls printLocations with an instance of class CompanyA as an argument). Class CompanyA
declares a method getLocations that overrides the one from class Company,
so this is the one that is called.To reason about programs that use dynamic binding, such as the one shown above, we can simply apply the principle we introduced above: assign a specification to each method of the program, and check that each method’s behavior complies with its specification, assuming that the behavior of method calls complies with the called methods’ specifications. Suppose we assign the strong specification to method getLocations in class CompanyA:
/**
* @post | result != null
* @post | result.length == 3
* @post | Arrays.stream(result).allMatch(e -> e != null)
*/
String[] getLocations() {
return new String[] {"Brussels", "Paris", "Berlin"};
}
When checking method printLocations, we need to determine which method is called by call company.getLocations(). Since the precondition of printLocations does not specify the precise class of argument company, we need to consider all possible callees. In this program, since the only method that overrides abstract method getLocations in class Company is the one in class CompanyA, we can assume the call complies with the specification of getLocations in class CompanyA. This way, we can conclude the correctness of printLocations.
This approach is modular, in the sense that if we modify a method, and the modified method still complies with its original specification, we can immediately conclude that the correctness of the program as a whole is preserved.
However, this approach does not deal optimally with another type of program modification: adding a new class that extends an existing class.
Indeed, suppose we extend the example program with the following class:
class CompanyB extends Company {
/**
* @post | result != null
* @post | result.length == 2
* @post | Arrays.stream(result).allMatch(e -> e != null)
*/
String[] getLocations() {
return new String[] {"Vienna", "Prague"};
}
}
By adding this class, we have enlarged the set of possible callees of call company.getLocations() in method printLocations. As a result, we need to re-verify method printLocations. In this case, we discover that it is not correct as-is.
In general, when applying the simple modular reasoning approach defined above to a program with dynamically bound calls, after adding a class to the program we need to re-check all methods that perform dynamically bound calls.
We conclude that the basic modular reasoning approach defined above is not adequate for reasoning about programs that use dynamic binding.
To solve this issue, we look, when checking a method, not at the specifications of the called methods of the call expressions that appear in the method, but at the specifications of the resolved methods. For example, when checking method printLocations, we only look at the specification of method getLocations in class Company. Furthermore, we check, when checking a method, not just that it complies with its own specification, but also that it complies with the specifications of all methods it overrides. In the example, we check that method getLocations in class CompanyA complies both with its own specification, and with the specification of method getLocations in class Company.
When adding a new class, we only need to check that its methods comply with the specifications of all methods they override. If so, we can immediately conclude that the correctness of the program as a whole is preserved.
In the example, there are two cases:
getLocations in class Company, then method printLocations is correct, but adding class CompanyB is incorrect because its getLocations method does not comply with the specification of method getLocations in class Company which it overrides.getLocations in class Company, then we need to update method printLocations. After fixing method printLocations, the program is correct. When adding class CompanyB, we only need to check that its method getLocations complies with the specification of getLocations in Company. Since it does, we can immediately conclude that adding this class preserves the correctness of the program as a whole.We summarize the basic principle of effective modular reasoning about programs with dynamic binding as follows:
If we apply this basic principe directly, we potentially have to verify a single method implementation against many different specifications. To avoid this, we can instead use a derived principle, that requires us to only check that 1) each method complies with its own specification, and 2) that each method’s specification strengthens the specifications of all methods it overrides. We say that a specification S strengthens another specification S’ if and only if each imaginable method that complies with S also complies with S’.
If a specification consists of a precondition and a postcondition, then we have the following property: specification S strengthens specification S’ if 1) the precondition of S weakens the precondition of S’, and 2) the postcondition of S strengthens the postcondition of S’.
For example, in the following sequence of specifications for a method abs, each next specification strengthens the preceding one:
/**
* @pre | false
* @post | true
*/
public static int abs(int x)
/**
* @pre | 0 <= x
* @post | true
*/
public static int abs(int x)
/**
* @pre | 0 <= x
* @post | 0 <= result
*/
public static int abs(int x)
/**
* @pre | true
* @post | 0 <= result
*/
public static int abs(int x)
/**
* @pre | true
* @post | false
*/
public static int abs(int x)
The first specification is the weakest possible one: it does not allow any calls of the method, so the method is free to crash or exhibit any behavior whatsoever. The last one is the strongest possible one, because it is unimplementable: since there exists no method implementation that satisfies postcondition false, it is vacuously true that every such implementation has the desired behavior (for any definition of “desired behavior” whatsoever).
If we assign a specification to each method of a class C, then in doing so, we define a behavioral type. We say an object O is of behavioral type C, if, for every method M of C, the behavior of a call of M on O complies with the specification of M in C.
(Notice that the behavioral type defined by class is defined entirely by its documentation; the implementation of a class is completely irrelevant to the behavioral type it defines. (But the implementation of class C is relevant to the question of whether the instances of class C are of the behavioral type C.))
We say a behavioral type D is a behavioral subtype of a behavioral type C if each object that is of behavioral type D is also of behavioral type C.
If the specifications of the methods of D that override methods of C strengthen the specifications of the overridden methods, then it follows that behavioral type D is a behavioral subtype of type C.
We say that a program respects behavioral subtyping if, for every class D of the program that extends a class C, it is the case that D is a behavioral subtype of C.
Using these definitions, we can rephrase the principle of modular reasoning about programs with dynamic binding as follows: if A) each method of a program complies with its specification, assuming that each object it interacts with is of the behavioral type given by its static type, and B) the program respects behavioral subtyping, and C) the specification of the program’s main method expresses the correctness of the program as a whole, then the program as a whole exhibits only correct behaviors.
Or, to phrase it as a slogan: Java’s static type checker ensures that a subclass D of a class C is a syntactic subtype of C; to achieve correct programs, we must ensure that D is a behavioral subtype of C as well.
In the literature on behavioral subtyping, some authors propose that the effective specification of a method should be the conjunction of the declared specification and any inherited specifications. (The conjunction of a specification with precondition P1 and postcondition Q1 and a specification with precondition P2 and postcondition Q2 is the specification with precondition “P1 or P2” and postcondition “(if old(P1) then Q1) and (if old(P2) then Q2)”.) In this approach, called specification inheritance, if the implementation of each method of a program complies with its effective specification, the program automatically complies with behavioral subtyping.
In this course, however, we do not apply specification inheritance; a method’s effective specification is exactly its declared specification. (Therefore, we can speak simply of “a method’s specification” without introducing ambiguity.)
We make one exception to this rule: if the Javadoc comment associated with a method M does not contain any specification clauses at all (i.e. no @pre, @post, @throws, @may_throw, @inspects, @mutates, @mutates_properties, @creates, @immutable, @peerObject, or @peerObjects clauses at all), and M overrides some method M’ that itself overrides all other methods that M overrides, then we define the specification of M as being identical to the specification of M’.
Note: the material in this section is outside the scope of the course and is provided for the information of interested students only.
For a much more detailed, formal, academic treatment of the approach to modular reasoning about programs that involve dynamically-bound method calls and the notion of behavioral subtyping described in this note, we refer interested students to Matthew J. Parkinson. Local reasoning for Java. PhD Thesis, Cambridge University, 2005.
Work on behavioral notions of subtyping in object-oriented programming goes back to the early nineties with work by America, Liskov and Wing, Leavens, and others; see the bibliography in Parkinson’s thesis. Some of this early work, however, confusingly discusses the problem in terms of substituting subtype objects for supertype objects. This is not a good way to think of the problem of modular reasoning about object-oriented programs. Most importantly, it invites confusing behavioral types with implementations. We repeat that a behavioral type is defined entirely by the type’s documentation, not by any implementations. The correct image is that of a single object that is of two behavioral types (one of which is a behavioral subtype of the other). One example of where the substitution narrative breaks down is if the supertype is an abstract class (or an interface): in that case, no object can exist whose class is the supertype.