Lecture 6: For-all, Intro to PBT

1 Purpose

Introduce for-all. Core of PBT: rather than hand-choosing input to pass to properties, let the computer.

2 Outline

At this point, we’ve written quite a few specifications. These have been, up until this point, generally been boolean predicates. We’ve used these both to describe properties (or invariants) about data: is a piece of data sorted, for example, to use to help build a specification for a sort function, but also, to describe what should happen when we call a given function: i.e., if we convert all other colors to black & white, none of them will be within a certain luminance of the given color, converted to black and white.

When we have used these specifications in tests, we have chosen particular inputs. For some data (e.g., our colors), we can exhaustively test all inputs, which forms a proof, a la truth table, that the function is indeed correct.

For others, like a sorting function, we have simply chosen a few inputs. This is disappointing for various reasons, not least of which, our specification should apply no matter the input! Part of the benefit of moving from a hard-coded input/output pair to a test based on a specification is that our test cases no longer depend upon us figuring out the output by hand. We simply need to write down the input, and the specification can run.

i.e., what we would like to write is:

(define-struct person [name age])
; A Person is a (make-person String Number)

;; sort-people : [List-of Person] -> [List-of Person]
(define (sort-people lop) 
  (sort lop (lambda (p1 p2) (<= (person-age p1) (person-age p2)))))

(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 (subset-of? l1 l2)
  (local [(define (count-occurrences e l)
            (length (filter
                     (λ(el)
                       (equal? el e))
                     l)))]
  (andmap (λ(e1) (= (count-occurrences e1 l1)
                    (count-occurrences e1 l2)))
          l1)))

(define (permutation l1 l2)
  (and (subset-of? l1 l2)
       (subset-of? l2 l1)))
       
(define (sort-people-prop l)
  (local [(define SORTED (sort-people l))]
    (and (sorted SORTED)
         (= (length l) (length SORTED))
         (permutation l SORTED))))

(check-property (for-all [(l [ListOf Person])]
                  (sort-people-prop l)))

What have we stated? That we want the property to not hold of some particular chosen inputs, but that we want it to hold for all lists of people. We are using the logical operator for-all from first-order logic, often written symbolically as \forall, but we are using it to lift out statement about a single list to a property that is now universally quantified. It is now a much more useful logical statement.

As a statement, it certainly expresses what we wish to be true. But does this code work? What could it do?

What do you think it should do?

Well, it doesn’t quite work. In particular, we need to teach the library how to generate Person’s, which we can do as:

(define Person (RecordOf make-person
                         (list person-name
                               person-age)
                         String
                         Integer))

ISL-Spec has a collection of types it already knows how to generate: Integers, Strings, Booleans, but also Lists, and Records. Lists require a generator for the type of the elements, and records require a constructor, list of field accessors, and generator for each field, as we see here.

How does this work?

Well, it can’t run on all inputs: that would take forever. So, it runs on a random sample of inputs. We’ll get into more detail later on how you might be able to tune what exactly "random" means here, but for now, imagine it tries a selection, with a bias towards smaller inputs (which are easier to deal with if it finds a counterexample).

More examples

Let’s define a property that reverse and append commute over lists. We’ll use lists of numbers.

(define (rev-app-prop l1 l2)
  (equal? (reverse (append l1 l2)) (append (reverse l2) (reverse l1))))

(check-property (for-all [(l1 [ListOf Integer])
                          (l2 [ListOf Integer])]
  (rev-app-prop l1 l2)))