7. Judging Specifications

7. Judging Specifications
	Chapter 17. Specification

Suppose you want to substitute one method for another. How do you compare the specifications?

A specification A is at least as strong as a specification B if

A’s precondition is no stronger than B’s
A’s postcondition is no weaker than B’s, for the states that satisfy B’s precondition.

For example, the method maybePrime can be replaced in any context by a method isPrime that returns true if and only if the integer is prime.

There are no infallible rules to write specifications, but there are some useful guidelines:

The specification should be coherent: it shouldn't have lots of different cases. Deeply nested if- statements are a sign of trouble, as are boolean flags presented as arguments.
The results of a call should be informative: Java’s HashMap class has a put method that takes a key and a value and returns a previous value if that key was already mapped, or null otherwise. HashMaps allow null references to be stored, so a null result is hard to interpret.
The specification should be strong enough: There’s no point throwing a checked exception for a bad argument but allowing arbitrary mutations, because a client won’t be able to determine what mutations have actually been made.
The specification should be weak enough: A method that takes a URL and returns a network connection clearly cannot promise always to succeed.


6. Shorthands		8. Lecture Notes