Lecture 6: Using LSL II

1 Purpose

Show more features from LSL

2 Outline

Important: Upgrade LSL if you haven’t already. Go to "Package Manager" in menu, type in lsl, hit "Update"

We’ve seen a few examples of the output from LSL when it finds counter-examples, but today we’re going to look into that output in more detail, and explain what the errors mean.

Consider this, very simple function that violates its contract:

Now, that is how blame looks when the function, individually, is violating its contract. It says that the function f had a contract violation, and that the contract expected an Integer but received the value #f. Contracts are ways of classifying sets of values (like all Integers), and each time a value is checked against a contract (as an input or an output to a function) it is checked to see if it belongs to that set. If it doesn’t, this type of violation occurs.

If, rather than using check-contract, or check-expect, we had called the function as:

(f 10)

f: contract violation

expected: Integer

given: #f

blaming: program (as server)

We get the same error, though without the context of having been run as part of a test. In DrRacket, the latter would also result in highlighting the contract that was violated (this doesn’t happen with test suites, since a single test suite may result in many errors, so highlighting would be confusing).

That’s a really simple case.

But sometimes the situation is a bit more complex. For example, consider this (quite artificial) code:

(: q (-> Integer Integer))

(define (q x)   (g x))

(: g (-> Integer Integer))

(define (g x)   (h x))

(: h (-> Integer Integer))

(define (h x)   #f)

(check-contract q)

-------------------- interaction-area tests > Unnamed test FAILURE params:     '(#<procedure:...yntax/interface.rkt:83:7> 100) name:       check-contract location:   eval:11:0 discovered a counterexample   counterexample: (q 0)   error:     [assert] h: contract violation       expected: Integer       given: #f       blaming: program (as server) -------------------- 0 success(es) 1 failure(s) 0 error(s) 1 test(s) run

(q 10)

h: contract violation

expected: Integer

given: #f

blaming: program (as server)

Now, clearly we would never write code exactly like this: two functions that do nothing but call another function. But, the phenomena is quite common: q will eventually return #f, which is a violation of its contract, but it isn’t really anything wrong with the body of q: it called g and g is supposed to return an Integer, so all should be well. The same is true of g. The actual fault is with h. Now, running this, as is, immediately identifies the problem, since we’ve given each function a contract.

Up until now, all the types we’ve used have been atomic: Integer, Boolean, etc. While we’ve showed you how you can use contract-generate to generate random instances of those values, we haven’t talked much about what we mean by "random". As it turns out, there are many different ways of generating random values.

The main thing we want to think about is the "distribution" of values. What that means is, what type of values are we likely to get. For example: if I am generating integers, what is the range of integers I want to get? Across that range, do I want numbers picked uniformly (as in, the biggest number is as likely as the smallest, is as likely as 0)?

There are a couple reasons why we might want to be more particular. One is that if we do find a counter-example, certain inputs may be easier to use to debug. Knowing that the function is buggy on 7 is more helpful than knowing it is buggy on 983491009120, even if both are the case.

It becomes even more extreme when we get to recursive data: lists can be of arbitrary length: how long do we want the examples to be? Knowing that a function is buggy on a list of length 500,000 is going to be very unhelpful; knowing that it is buggy on a list of length 5 could be very useful.

There are other factors that can lead us to want to define custom generators, but for now, we’ll just focus on defining alternative generators for some of the built-in atomic types, starting with numbers.

Aliases. We showed, on the very first day, that LSL allows us to define type aliases: contracts that mean the same thing as other contracts.

(define-contract NiceInteger Integer)

This might allow us to write slightly more illuminating signatures, but on its own, doesn’t change anything about how the can use the contract. In order to do that, we need to know how to build contracts. There are a couple different types, but for now, the only type we need to think about are called Immediate contracts. These are contracts for values that can be checked directly using boolean predicate functions (e.g., integer?). To make a new one we use Immediate, which takes several arguments (written in the keyword style of big-bang), some of which are optional:

(define-contract Even (Immediate (check (lambda (x) (and (integer? x) (even? x))))                                  (generate (lambda (fuel) (* 2 (contract-generate Integer fuel))))))

This says that a new contract, Even. It is an Immediate contract, which means that it can be used to check values directly; this is different from, e.g., functions, which have to be wrapped and checked on use. There are several arguments, but the two passed here are check, which is a predicate that says how to recognize values of this type, and generate, which is a function that, given a natural number fuel (and indication of how large a value to create), creates a random example. In this case, we use the built-in generation for Integer, multiplying by 2 to get an even number.

Exercise: Define a different version of Even, where instead of using contract-generate, you use random. Think about how you might use (or not use) the fuel argument.

We can try this out by defining a (buggy) function as follows:

(: plus1 (-> Even Even))

(define (plus1 n)   (add1 n))

Which can be determined to be buggy via random generation:

(check-contract plus1)

-------------------- interaction-area tests > Unnamed test FAILURE params:     '(#<procedure:...yntax/interface.rkt:83:7> 100) name:       check-contract location:   eval:17:0 discovered a counterexample   counterexample: (plus1 -2)   error:     [assert] plus1: contract violation       expected: Even       given: -1       blaming: program (as server) -------------------- 0 success(es) 1 failure(s) 0 error(s) 1 test(s) run

You could, of course, generate the even numbers in some other way: this function will distribute them in the same way as Integer does, but perhaps you are only concerned with even numbers under 100, and want to ignore the fuel parameter.

(define-contract EvenUnder100 (Immediate (check (lambda (x) (and (integer? x)                                                                  (even? x)                                                                  (< x 100)                                                                  (>= x 0))))                                          (generate (lambda (_) (* 2 (random 0 50))))))

We can also leave out some of these fields (and there are more we’ll see later). For example, we could define a contract that cannot be used to generate data at all, but could be used to check the return types by only including the check field:

(define (in-order? l)   (cond [(empty? l) #t]         [(cons? l) (and (andmap (lambda (x) (<= (first l) x)) (rest l))                         (in-order? (rest l)))]))

(define-contract InOrder (Immediate (check in-order?)))

This pattern is common enough that you can write this more concisely as:

(define-contract InOrder2 in-order?)

Anytime a predicate f is used in a position a contract is expected, it is treated as (Immediate (check f)).

Lists. We saw before the built-in support for Lists.

As an exercise, if you did want to have a list of any element (rather than a list of integers, or strings), how could you define it?

You can also define lists of a fixed (rather than arbitrary) size as:

(define-contract TwoInts (Tuple Integer Integer))

You can see that it will only generate lists of size two:

> (contract-generate TwoInts)

'(-12 -24)

> (contract-generate TwoInts)

'(4 48)

> (contract-generate TwoInts)

'(-20 -4)

> (contract-generate TwoInts)

'(-3 25)