Lecture 21: Temporal Specifications

1 Purpose

Introduce Temporal Specifications

2 Outline

Up until now, all specifications, no matter how sophisticated, have been about independent function calls. The most sophisticated example we have seen in class, probably, involved the error correction, as it was a property about multiple functions working together. Today we are going to start to see a technique that can allow us to cover cases of things happening in a certain order.

Let’s think about an example: a function to generate unique numbers. Now, generating random numbers is easy, and if you choose a sufficiently large range, then they might always be unique:

(define (maybe-unique)   (random 1000))

But how could we write down a specification to check that no numbers were duplicated? Well, we could write a property that ran it many times and checked that there were no duplicates:

(define (do-n-times n f)   (build-list n (lambda (_) (f))))

(require racket/list)

(length (remove-duplicates (do-n-times 1000 maybe-unique)))

635

Which shows us that, indeed, this function will not always return unique numbers (a pencil and paper proof could have shown that, as well!).

The property we are capturing here is something that holds across many invocations.

LSL has built-in support for expressive temporal specifications via a contract Record. This records values across invocations by mutating a given defined value. We can use this to capture the same uniqueness invariant as:

(define-contract UniqueList (lambda (l) (equal? (length l) (length (remove-duplicates l)))))

(: ids UniqueList)

(define ids empty)

(: maybe-unique2 (-> (AllOf Natural (Record ids))))

(define (maybe-unique2)   (random 1000))

We can see this goes wrong if we call the function enough:

(do-n-times 100 maybe-unique2)

contract violation

expected: UniqueList

given: '(669 124 507 732 276 946 307 646 781 24 734 84 14

959 356 679 849 304 517 43 474 694 898 149 262 342 333 213

972 628 164 947 352 634 347 489 572 416 440 367 481 149)

In detail, what we’ve written for the contract for maybe-unique2 is that it returns a Natural and that it Records values into the ids definition. If ids just had the contract (List Natural) (or had no contract at all), this wouldn’t check anything: it would just log all values that were returned from the function. Indeed, we can inspect ids after running maybe-unique2 and seeing that it has been modified:

> ids

'(669   124   507   732   276   946   307   646   781   24   734   84   14   959   356   679   849   304   517   43   474   694   898   149   262   342   333   213   972   628   164   947   352   634   347   489   572   416   440   367   481)

But since ids has a contract that says it has to be a unique list of numbers, every time it is modified, that invariant is checked, and so as soon as maybe-unique2 fails to return a new value (will vary, since it is random), a contract error will result. Note that, unlike the error above, this doesn’t have the erroneous duplicate last value, since the contract error prevented it from being added.

Exercise: define a contract that ensures that an (-> Integer Integer) function f is never called with the same input more than once.

(: inp UniqueList)

(define inp empty)

(: f (-> (AllOf Integer (Record inp)) Integer))

(define (f x) x)

There is also a more flexible version of Record that we can use, where rather than just cons’ing the new value to a list of all existing ones, we incorporate it in some other way.

For example, let’s say we wanted a function large-random that returned random natural numbers, but we wanted the average of the outputs to be above 10 (even if individual numbers could go below). This means that if we have produced many high numbers, it’s fine to produce some small ones, but it wouldn’t be okay for the first number produced to be below 10.

While we could record every output, having to recalculate the average every time is unnecessary, given that the only thing we need to know is the average, which can be updated if we know the total number of numbers seen and the current average.

(define-struct avg [val count])   (define (update-avg a n)   (let* ([new-count (add1 (avg-count a))]          [new-val (+ (/ n new-count) (* (avg-val a) (/ (avg-count a) new-count)))])     (make-avg new-val new-count)))   (define (avg-above-ten? a)   (or (zero? (avg-count a))       (> (avg-val a) 10)))   (: rnd-avg avg-above-ten?) (define rnd-avg (make-avg 0 0))   (: large-random (-> (AllOf Natural (Record update-avg rnd-avg)))) (define (large-random)   (random 100))   (do-n-times 50 large-random)

Exercise: Given functions f and g, define trace contracts that ensure that g is never called immediately after itself, and the same with h. i.e., they are always interleaved.

(: ghst (OneOf (Constant 'any-next)                (Constant 'g-next)                (Constant 'h-next)))

(define ghst 'any-next)

(define (g-call st _)   (cond [(equal? st 'any-next) 'h-next]         [(equal? st 'g-next) 'h-next]         [(equal? st 'h-next) 'error]))

(: g (-> (AllOf Integer (Record g-call ghst)) Integer))

(define (g x)   (add1 x))

(define (h-call st _)   (cond [(equal? st 'any-next) 'g-next]         [(equal? st 'g-next) 'error]         [(equal? st 'h-next) 'g-next]))

(: h (-> (AllOf Integer (Record h-call ghst)) Integer))

(define (h y)   (* y 10))