Lecture 24: 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))))

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

634

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: '(899 724 265 844 263 365 206 767 377 333 305 339

308 581 58 725 927 520 357 659 403 390 162 551 181 734 228

986 287 864 755 963 272 237 944 409 225 813 415 117 703 446

732 698 436 777 263)

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

'(899   724   265   844   263   365   206   767   377   333   305   339   308   581   58   725   927   520   357   659   403   390   162   551   181   734   228   986   287   864   755   963   272   237   944   409   225   813   415   117   703   446   732   698   436   777)

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.

State? You may have noticed, there is an odd thing going on: ids has been modified by the contract. This is, of course, the point, but especially for testing, this may be a problem, as you may not want changes to persist.

To support this, LSL has a primitive with-traces that can be wrapped around any expression. If so, then any modifications done by Record within that are reset after the with-traces finishes. Note that contract violations will still produce errors, but even in the error case, the original value of any values modified by Record will be restored.

We can see this by changing the above to:

(with-traces (do-n-times 100 maybe-unique2))

Note the similar error, but now if we inspect ids, we do not see anything recorded.

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 g and h, 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))