Lecture 10: Recursive Contracts🔗

1 Purpose🔗

Introduce recursive contracts

2 Outline🔗

A few days ago, we saw how we could use OneOf to build contracts that are enumerations of other contracts. For example, we can define a Bit as follows:

(define-contract Bit (OneOf (Constant 0) (Constant 1)))

As it turns out, just as we use itemizations in signatures in comments to define self-referential (or recursive) data:

(define-struct leaf [value])

(define-struct node [left right])

(define-contract (Leaf X) (Struct leaf [X]))

(define-contract (Node X Y) (Struct node [X Y]))

; A [Tree X] is one of:

;  - (make-leaf X)

;  - (make-node [Tree X] [Tree X])

We can do the same with contracts, defining the same binary tree as follows:

(define-contract (Tree X) (OneOf (Leaf X) (Node (Tree X) (Tree X))))

This will automatically create a predicate for checking and a generator for generating trees, but it’s a good exercise to do it by hand:

(define (inttree? t)   (or (and (leaf? t) (integer? (leaf-value t)))       (and (node? t)            (inttree? (node-left t))            (inttree? (node-right t)))))

(define (inttree-generate fuel)   (cond [(zero? fuel) (make-leaf (contract-generate Integer fuel))]         [else (if (< (random) 1/2)                   (make-leaf (contract-generate Integer fuel))                   (make-node (inttree-generate (sub1 fuel))                              (inttree-generate (sub1 fuel))))]))

(define-contract IntTree (Immediate (check inttree?)                                     (generate inttree-generate)))

Now let’s start by writing some simple functions on trees that have Integer’s as values:

(: height (-> IntTree Natural))

(define (height t)   (cond [(leaf? t) 0]         [(node? t) (add1 (max (height (node-left t)) (height (node-right t))))]))

(check-expect (height (make-leaf 0)) 0) (check-expect (height (make-node (make-leaf 0) (make-node (make-leaf 0) (make-leaf 0)))) 2)

2 success(es) 0 failure(s) 0 error(s) 2 test(s) run

We can of course use check-contract to exercise the function on many different trees, though this only checks that it always returns a Natural:

(check-contract height)

1 success(es) 0 failure(s) 0 error(s) 1 test(s) run

Of course, we can do better than this. A theorem we might want to hold is that given a tree, if we nest it to the left (or right) side of a node that has a leaf on the other side, the resulting tree has height one greater. We could express that as:

(: height-rec-prop (-> IntTree True)) (define (height-rec-prop t)   (and (equal? (add1 (height t))                (height (make-node t (make-leaf 0))))        (equal? (add1 (height t))                (height (make-node (make-leaf 0) t))))) (check-contract height-rec-prop)

1 success(es) 0 failure(s) 0 error(s) 1 test(s) run

This is part of what we need for height to be correct – what else do we need? Could you create a buggy implementation of height that still passes this? It turns out, this somewhat covers the recursive case, which is good, but nothing ensures that the base case is correct. We could either add that as a separate property:

(: height-base-prop (-> True)) (define (height-base-prop)   (equal? (height (make-leaf 0)) 0)) (check-contract height-base-prop)

1 success(es) 0 failure(s) 0 error(s) 1 test(s) run

Now we almost have it. But we are only ensuring that we have a size metric: we aren’t showing that height isn’t counting nodes beyond a single path. You can improve that be adding a third property:

Thanks to a previous CS2800 student for pointing this out!

(: height-sides-prop (-> IntTree True)) (define (height-sides-prop t)   (equal? (add1 (height t))           (height (make-node t t)))) (check-contract height-sides-prop)

1 success(es) 0 failure(s) 0 error(s) 1 test(s) run

This makes sure that your number only counts down one side.