Lecture 5: Relational Specifications
1 Purpose
Reinforce design / specification recipe, leading towards PBT.
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)))))
;; collatz-trace : Number -> [List-of Number]
(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 it 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.
Error correction
Now, let’s look at another example. Let’s consider an important problem: how to recover data that is corrupted. This is incredibly important for radio transmision, as wireless signals are prone to interference, but there are many other applications.
This is always done by introducing some amount of redundancy in the data. A simple way to do this, known as a repetition code, involves repeating the data multiple times.
Let’s say we have a sequence of bits, represented as:
; A Bit is one of:
; - 0
; - 1
; A Packet is a Bit
; A Message is a [List-of Packet]
We want to be able to correct some amount of errors. In particular, we’ll split our BitString into "packets", each a single bit, and our goal is to be able to introduce a single error (randomly) into each packet. If we did this without changing the data, there would be no way of recovering, as a single change would change the entire packet. But, we will first encode the packets into a larger packet (of size 3), then introduce the error, and then decode. Our goal is to be able to recover the original message regardless of how (or if) the errors are introduced.
Let’s formally specify what we just described in English:
; A TripletPacket is a (list Bit Bit Bit)
; encode : Packet -> TripletPacket
; ...
; decode : TripletPacket -> Packet
; ...
; message-recovery-prop : Message -> Bool
(define (message-recovery-prop msg)
(local [(define (mutate c b) (if c (if (= b 0) 1 0) b))
(define (introduce-error triplet)
(local [(define idx (random 4))]
(list (mutate (= idx 0) (list-ref triplet 0))
(mutate (= idx 1) (list-ref triplet 1))
(mutate (= idx 2) (list-ref triplet 2)))))]
(equal? (decode (map introduce-error (encode msg))) msg)))
Note that at this point, we’ve described the data (that we’ll allow three bits), and how we want encoding / decoding to be able to handle errors (up to one bit mutation without any loss of information), but we haven’t said anything about the implementation.
In this case, the implementation is pretty straightforward: we simply duplicate the bit, and to decode, take the majority. We can then check that the property holds with a few examples.
; encode : [List-of Packet] -> [List-of TripletPacket]
(define (encode msg)
(map (lambda (p) (list p p p)) msg))
; decode : [List-of TripletPacket] -> [List-of Packet]
(define (decode msg)
(map (lambda (t) (if (> (foldr + 0 t) 1) 1 0)) msg))
(check-property (message-recovery-prop (list 0 0 0 0 0)))
(check-property (message-recovery-prop (list 1 0 1 1 0)))
Now, it’s a little bit dissappointing that we are checking this property with just a few, hand-chosen messages. We’ll come back to that.
Specification Last time, 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 class, 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 mantain 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. Recall the function shortest-string from last week:
; shortest-string : [List-of String] -> String or #f
(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-property (shortest-string-prop (list "a" "bb" "CCC")))
(check-property (shortest-string-prop (list)))
(check-property (shortest-string-prop (list "aa" "b" "c" "dd")))
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.
Can you think of any other relational properties?
Think about sorting. Say you have a data definition for a person, with a name and an age:
(define-struct person [name age])
; A Person is a (make-person String Number)
And you want to write a function sort-people that sorts people by their age, ascending:
;; sort-people : [List-of Person] -> [List-of Person]
(define (sort-people lop) ...)
Writing unit tests for this is problematic, as you end up with multiple possibilities:
(check-expect (sort-people (list (make-person "A" 19) (make-person "B" 19)))
(list (make-person "A" 19) (make-person "B" 19)))
(check-expect (sort-people (list (make-person "A" 19) (make-person "B" 19)))
(list (make-person "B" 19) (make-person "A" 19)))
Both of these options are correct, and indeed, if you want to allow different sorting algorithms, it’s probably quite important not to enforce a certain ordering of otherwise equivalent elements.
How do we avoid this? By defining the notion of sortedness as a property, and making our specification be that sort-people results in a sorted list!
(define (sorted l)
(cond
[(empty? l) #t]
[(cons? l) (and (andmap (lambda (p) (>= (person-age p) (person-age (first l))))
(rest l))
(sort-people-prop (rest l)))]))
(define (sort-people-prop l)
(sorted (sort-people l)))
What is this expressing? That for every element in the list, everything later in the list has an age greater than or equal to it. That captures the notion of sortedness.
Now I can write tests in a form that allows any correct sorting algorithm:
(check-property (sort-people-prop (list (make-person "A" 19) (make-person "B" 19))))
Now, when we are coming up with these specifications, we do have to be careful: one benefit of unit tests is that they had us think about the input & the output, and write them down carefully. Just as our code can have bugs, so can our specifications, and they may not be obvious, at first. So often, we want to still include unit tests. In this case, it would be good to have unit tests for lists that did not have duplicate ages (and thus did not result) in ambiguity.
But if we just look at the specification, do we see any issue?
One problem: we are no longer ensuring that the same elements, or even any elements, come out of our function. We could define sort-people to return the empty list on all input and it would pass this specification, as indeed, the empty list is sorted!
Clearly, if we included some unit tests, we would rule out that possibility, but we can also extend our property to include other details. For example, we might want to ensure that the length of the input & output lists were the same, and that all elements in the input occurred somewhere in the output.
Figure out how to write those two as properties, and extend sort-people-prop to include them both.
(define (elements-in? l1 l2)
(andmap (lambda (p1) (ormap (lambda (p2) (equal? p1 p2)) l2)) l1))
(define (sort-people-prop1 l)
(local [(define SORTED (sort-people l))]
(and (sorted SORTED)
(= (length l) (length SORTED)
(elements-in? l SORTED)))))