Lecture 8: Relational Specifications

1 Purpose

Reinforce design / specification recipe.

2 Outline

Soundness & Completeness

We can distinguish between proof and truth. A logical system allows us to prove certain things, whereas truth is a notion outside of any particular mechanism of proof.

Consider the halting problem. Any given program in a deterministic language either halts or doesn’t halt (truth), but the halting problem famously showed that there is no program that, given an arbitrary program as input, can determine if that program halts (proof).

Or, the Collatz conjecture. Does this program terminate for all input? Clearly, there is an answer (either it does or doesn’t), but in this case, we don’t even know, and we certainly don’t know how to prove it. If you do, would be very cool!

(define (collatz n)   (if (<= n 1)       n       (if (even? n)           (collatz (/ n 2))           (collatz (+ (* n 3) 1)))))

(define (collatz-trace n)   (if (<= n 1)       (list n)       (if (even? n)           (cons n (collatz-trace (/ n 2)))           (cons n (collatz-trace (+ (* n 3) 1))))))

We can relate these two ideas with two words: soundness and completeness. In logic, a proof system is sound if all provable statements are true, but there may be true statements that are not provable. A proof system is complete if all true statements are provable, but possibly there are false statements that are also provable. Clearly, the best case is a sound and complete proof system, but such things may not be possible.

The same idea applies to specifications.

A specification is sound if all implementations that it admits are correct (this is our notion of "truth"), but it may not admit all correct implememations.

A specification is complete if it admits all correct implementations (our notion of truth), but it may also admit incorrect implementations.

Specification Last week, we introduced the idea of a specification, and how it fits into the design recipe. Specifications allow us to express, precisely in code, the behavior of our functions. This is more precise than in text, and can be more obvious to understand than in unit tests, even if we include many many unit tests. Indeed, for the color->b&w example from last week, we could have included unit tests for all of the inputs, but seeing:

(check-expect (color->b&w RED) 76.245) (check-expect (color->b&w BLUE) 29.07) (check-expect (color->b&w GREEN) 149.685) (check-expect (color->b&w YELLOW) 225.93) (check-expect (color->b&w PURPLE) 105.315)

Is not particularly informative. It doesn’t communicate, in particular, that what we want is that the distance between any pair of colors is at least 20 points of luminance. And indeed, if we add a new color, nothing in these tests will let us know that we should be aiming to maintain that invariant. Whereas, with our specification, adding a new color will immediately cause the tests for all the other colors to ensure that they are distinguishable from our new color.

Beyond comprehension, there are some specifications that we simply cannot express as unit tests. Consider a function shortest-string:

(define (shortest-string los)   ...)   (define (shortest-string-prop l)   (let ([min-len (string-length (shortest-string l))])     (andmap (lambda (s) (>= (string-length s) min-len)) l)))   (check-expect (shortest-string-prop (list "a" "bb" "CCC")) #t) (check-expect (shortest-string-prop (list)) #t) (check-expect (shortest-string-prop (list "aa" "b" "c" "dd")) #t)

If we wish to express that our function returns the shortest string in the list, we need to be able to account for the fact that there could be multiple shortest strings. One possible way to do this with unit tests is that we specify that we want the first shortest string, or the last, or the nth, in the case of a tie. But this is an unpleasant thing to do when writing a specification, because we are overspecifying: we are including details that are not relevant. A user of this function shouldn’t care, as any of those options are fine! By switching to express this as a property, we get away from this problem, as we can directly express this property.

Technically, what this allows us to do is express relational properties. Unit tests can only express function input/output pairs, which means, in particular, that while multiple inputs can map to the same output, a single input cannot map to multiple outputs. Often, this is fine, but sometimes, we want to be able to express exactly this: that there is a relation between the input and output, captured by some predicate. In this case, the predicate is that the output is at least as short as any other string in the input list.