About this paper
Teaching Quality OOP by Yishai A. Feldman, published March 2005 (see the link for full citation).
Notes
One of the points made in my book Object-Oriented Programming the Easy Way is that objects should be specified by their interfaces through contracts, which say what messages the objects respond to, how you use them, and what happens as a result.
While it is up to any one object to decide how it responds to messages, we need to know whether that object represents a useful addition to our system. In other words, we want to know what the object will do in response to what messages. (Page 61)
The book Structure and Interpretation of Computer Programs says the same thing. An abstract data type has a collection of things that can be done, and stuff that happens when you do it.
In general, we can think of data as defined by some collection of selectors and constructors, together with specified conditions that these procedures must fulfill in order to be a valid representation. (§2.1.3)
This seems evident. Knowing that I have a int count(), a boolean contains(Object o) and a void add(Object o) method is insufficient, I need to know how they interact before I can use them. For an array, given:
int x = a.count();
a.add(anObject);
int y = a.count();
you would always expect y - x == 1. For a set, it would depend on the content of the collection before addition; it could be 1 or 0. Knowing what methods are called is insufficient to know what type I am dealing with.
Why is it, then, that programming languages give you types for expressing the methods on an object, but not what they do or how they relate? Why does a Java interface, a Swift protocol, or a C++ abstract class only have the part of the contract related to names, not behaviours?
Famously, the Eiffel language addresses this, and it’s here that we come into contact with the paper that is the topic of this post. Eiffel, and its underlying theory, is well-described in the book Object-Oriented Software Construction by Bertrand Meyer, CTO of Eiffel Software and researcher at ETH Zurich. Feldman wanted to teach his students the theory of “Quality Software” based on two principles that are well-described in OOSC:
- Design by Contract, because it’s more approachable and usable than formal methods, and more useful than testing; and
- Command-Query Separation, because it isolates state changes, making it easier to draw conclusions about the behaviour of a software system.
But he didn’t want to teach them Eiffel, because:
it might leave the students with the mistaken and harmful impression that quality programming is confined to one language. (§3)
Additionally, OOSC does not include any exercises, so is not useful as a teaching support book. I will note here that Meyer has also written A Touch of Class, which does have supporting teaching material including exercises, but still uses the Eiffel language and therefore only solves half of the author’s problems.
Feldman taught the theory from OOSC using Eiffel notation, and encouraged students to complete exercises that were in variants of the Java programming language. Tools available at the time read the contract out of special additions to the class’s Javadoc comments, and modified the source code to include assertions at the relevant points in execution.
This led me to wonder about modern Java syntax, and whether it’s possible to make a similar tool using Java’s annotation features so that programmers don’t have to worry whether a source conversion tool has introduced errors, or trace changes to the source code when working back from a failure report to the broken source.
The answer is yes, and so now the Labrary can offer Java by Contract as a tool for designing Java types by contract. It encodes the parts of the contract as names of methods to invoke that return boolean, failing if the answer is false. A rewrite of the Map interface from page 13 of the paper is given below.
public interface Map {
/**
* Does the key k appear in the map?
*/
@Precondition(name = "nonNullK")
@Postcondition(name = "inMapIffInKeys")
boolean has(Object k);
default boolean nonNullK(Object k) {
return (k != null);
}
default boolean inMapIffInKeys(Object k, Boolean result) {
return (result == this.keys().has(k));
}
/**
* The value of the map at key k, null if undefined.
*/
@Precondition(name = "nonNullK")
@Postcondition(name = "nonNullValueIffHasKey")
Object item(Object k);
default boolean nonNullValueIffHasKey(Object k, Object ret) {
return ((ret != null) == this.has(k));
}
/**
* Associate key k with value v.
*/
@Precondition(name = "nonNullKeyAndValue")
@Postcondition(name = "hasK")
@Postcondition(name = "itemForKIsNowV")
void put(Object k, Object v);
default boolean nonNullKeyAndValue(Object k, Object v) {
return ((k != null) && (v != null));
}
default boolean hasK(Object k, Object v, Void result) {
return this.has(k);
}
default boolean itemForKIsNowV(Object k, Object v, Void result) {
return (this.item(k) == v)
}
/**
* Remove key k and associated value from map.
*/
@Precondition(name = "nonNullK")
@Postcondition(name = "doesNotHaveK")
void prune(Object k);
default boolean doesNotHaveK(Object k, Void result) {
return !this.has(k);
}
/**
* The set of all keys in the map.
*/
@Postcondition(name = "nonNullReturn")
ReadOnlySet keys();
default boolean nonNullReturn(ReadOnlySet result) {
return (result != null);
}
}
This approach lets us write contract conditions that have full access to the internal state of the objects they are implemented on, so internal invariants can be verified in addition to the properties explored through the interface (by specifying them on the implementing class, not on the declaring interface). As a few pages of the paper are dedicated to the author’s (and the class’s) experience with various design by contract tools and their shortcomings, it’s valuable to explore this space and come up with better approaches. I hope that Java by Contract is a useful addition.
Feldman additionally notes that the Java class library, including the Collections library, violates the Command-Query Separation principle. He even notes that the language does: the construct:
x++;
is both a command (increment x) and a query (what value did x previously have?) in a single expression. The early exercises in his class instruct students to write CQS-satisfying library objects (hence the Map example above), which the subsequent exercises build on.
Feldman left academia the year after this paper was written, and is now at IBM Research. That means the trail of development of this class has run out, and we cannot say how the teaching would have adapted to the subsequent decade of progress in Java.
