Lecture 8: PBT generators
1 Purpose
Sometimes you you need special generators.
2 Outline
Nesting for-all
(define (prop y) (if (< y 3)
(for-all [(x Integer)] (equal? (* x y) (* y x)))
(for-all [(x Integer)] (equal? (* x y 2) (* y x)))))
(check-property (for-all [(y Integer)] (prop y)))
Running more tests
(qc:with-medium-test-count (qc:quickcheck (for-all [(y Integer)] (equal? (* y 2) (+ y y)))))
Back to error correction
Last week, we wrote a specification for a simple error correction strategy. The specification we wrote was:
; A Bit is one of:
; - 0
; - 1
; A Packet is a Bit
; A Message is a [List-of Packet]
; A TripletPacket is a (list Bit Bit Bit)
; 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))
; 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)))
Now we can make our testing much better, by randomly generating messages. First, we’ll define how to generate Bits, and using that, Message. We’ll use qc:sized, which we saw yesterday, and takes as input a function from number to generator, and passes it random natural numbers.
(define Bit (qc:choose-one-of (list 0 1)))
(define Message (qc:sized (λ(len) (qc:choose-list Bit len))))
(check-property (for-all [(m Message)] (message-recovery-prop m)))
Sorting
You might recall insertion sort from Fundies 1. It’s not a terribly efficient sorting algorithm, but it’s also not terribly inefficient, and the code is straightforward to write:
(define L0 (list))
(define L1 (list 1))
(define L2 (list 2 3 5))
(define L3 (list 6 10 -2))
; isort : [List-of Number] -> [List-of Number]
; sorts the given list of numbers in ascending order
(check-expect (isort L0) L0)
(check-expect (isort L1) L1)
(check-expect (isort L2) L2)
(check-expect (isort L3) (list -2 6 10))
(define (isort l)
(cond [(empty? l) l]
[(cons? l)
(insert (first l)
(isort (rest l)))]))
; insert : Number [List-of Number] -> [List-of Number]
; put the number at the right place in a _sorted_ list
(check-expect (insert 1 L0) (list 1))
(check-expect (insert 1 L2) (list 1 2 3 5))
(check-expect (insert 4 L2) (list 2 3 4 5))
(define (insert n l)
(cond [(empty? l) (list n)]
[(cons? l)
(if (< n (first l))
(cons n l)
(cons (first l) (insert n (rest l))))]))
It works by inserting the first element at the right place into the result of sorting the rest; recursively.
Now, you can certainly test isort using PBT: generate lists, sort them, check that the results satisfy the predicate. But can you do the same for insert? You could use ==>, but almost no randomly generated lists will be sorted, so you will likely just end up not passing anything to insert. Need to do something else.
To do this, we want to define our own generator, this time for sorted lists.
There are multiple ways of doing this, but the strategy that we’ll use is to generate one number at a time, each time, choosing a number larger than the last. This will be a recursive function that takes a length as an input. We’ll then wrap this up with a generator than first generates a number and then uses that to make a sorted list of that length.
(define INTERVAL 10000)
(define (mkSortedList k n l)
(cond [(zero? k) (qc:generator-unit l)]
[else (qc:generator-bind
(qc:choose-integer n (+ n INTERVAL))
(λ(m) (mkSortedList (sub1 k) m
(append l (list m)))))]))
(define SortedList (qc:sized (λ(len) (mkSortedList len 0 empty))))
Now we can define sorted, which we can use to not only double check our sorted list generation, but use that to test insert:
(define (sorted l)
(cond [(empty? l) #t]
[(cons? l) (and (andmap (λ(x) (< (first l) x)) (rest l))
(sorted (rest l)))]))
(check-property (for-all [(l SortedList)] (sorted l)))
(check-property (for-all [(l SortedList)
(n Integer)]
(sorted (insert n l))))
Generating balanced trees
Recall from HW2, we defined binary trees as:
(define-struct leaf [value])
(define-struct node [left right])
; A [Tree-of X] is one of:
; - (make-leaf X)
; - (make-node [Tree-of X] [Tree-of X])
For homework, you defined a predicate to ensure that a given tree was balanced. What we want to do now is define a generator that produces only balanced trees. How might we do that? Well, following the idea from our sorted lists, we might choose a random height, at the top: then we know that one subtree must have that height minus 1, and the other subtree can either be the same height, or of height one smaller. Using those new heights, we can recursively generate the subtrees.
(define (mkTreeHeight k elem-gen)
(cond [(<= k 1) (qc:generator-bind
elem-gen
(λ(x) (qc:generator-unit
(make-leaf x))))]
[else
(qc:bind-generators
([decrease (qc:choose-one-of (list 0 1))]
[full-height (mkTreeHeight (- k 1) elem-gen)]
[other-side (mkTreeHeight (- k 1 decrease) elem-gen)]
[side (qc:choose-one-of (list 'left 'right))])
(cond [(symbol=? side 'left)
(make-node full-height other-side)]
[(symbol=? side 'right)
(make-node other-side full-height)]))]))
(define BalancedTree (qc:generator-bind (qc:choose-integer 0 10)
(λ(n) (mkTreeHeight n (qc:choose-integer 0 0)))))
(check-property (for-all [(t (qc:choose-list BalancedTree 10))]
#f))