Lecture 4: Using LSL
1 Purpose
Show how LSL has features to support expressing types and properties.
2 Outline
LSL has many features that support specifying and verifying code. Up until now, we’ve been using features that exist in ISL+. Today we’ll start introducing features in LSL, which will make it easier to write & check specifications.
The first feature, which we show in a simple way here, is that we can write signatures as code (called contracts), rather than as comments. Here, we indicate that p1 is a function (written with ->) that takes three Boolean inputs (P, Q, and R) and returns a Boolean (the last argument to the -> in the signature is the return type).
(: p1 (-> Boolean Boolean Boolean Boolean))
(define (p1 P Q R) (or P (and Q R)))
This is then checked every time the function is called. e.g., see the error I get if I pass a number as the first argument, not a boolean:
(p1 1 #t #f) p1: contract violation
expected: Boolean
given: 1
blaming: program (as client)
Note that, within DrRacket, if you run examples in the Interactions window, the contract that is violated will be highlighted, which is important in cases like this when there are multiple Booleans in the contract for p1!
There are built-in contracts for many of the atomic types:
Exercise: Write a function with signature for a function divisible-by-5? that takes an Integer and returns a Boolean. Try calling it on different inputs and see what errors you get. Also, try writing the function incorrectly, returning the Strings "true" and "false" and see what errors you get.
Just like you might write, in a comment, "a HeartBeat is a Natural", you can define new contracts as aliases to old ones:
(define-contract HeartBeat Natural)
After doing this, you can now use HeartBeat anywhere you would have used Natural.
But there is quite a bit more that LSL can do with contracts. In particular, most come with a way of generating random examples of it:
> (contract-generate HeartBeat) 46
> (contract-generate Real) 4.560428263752044
While generating a single random example is limited, what this allows LSL to do is randomly exercise your functions: it can generate random arguments, call your functions, and ensure that the return types satisfy their contracts. This is a general technique, avalailable in some form via library in most languages, and typically called "Property Based Testing".
For example, let’s say we had a my-abs function that took in Integers: if it works correctly, it should always return Naturals. If we accidentally got the branches wrong:
(: my-abs (-> Integer Natural))
(define (my-abs x) (if (< x 0) x (* x -1)))
I can check the contract using check-contract, which will have LSL generate examples of the inputs and pass them to the function, ensuring the output satisfies the output contract:
(check-contract my-abs)
--------------------
interaction-area tests > Unnamed test
FAILURE
params: '(#<procedure:...yntax/interface.rkt:83:7> 100)
name: check-contract
location: eval:9:0
discovered a counterexample
counterexample: (my-abs -1)
error:
[assert] my-abs: contract violation
expected: Natural
given: -1
blaming: program (as server)
--------------------
0 success(es) 1 failure(s) 0 error(s) 1 test(s) run
We get a contract violation. It tells us the number it got that was not a Natural (since it is negative). Now we can go and fix the code. Here’s another way of using it:
Let’s say I was writing a function to convert numeric grades to letter grades:
(: letter-grade (-> Integer String))
(define (letter-grade n) (cond [(>= n 90) "A"] [(>= n 80) "B"]))
But I forgot the last few cases. I can quickly find this problem by running (check-contract letter-grade). In this case, it’s not a contract violation that is discovered, but an error (missing cond case), but LSL is able to use the signature we gave in order to generate sensible input in order to find that problem:
(check-contract letter-grade)
--------------------
interaction-area tests > Unnamed test
FAILURE
params: '(#<procedure:...yntax/interface.rkt:83:7> 100)
name: check-contract
location: eval:12:0
discovered a counterexample
counterexample: (letter-grade -1)
error:
[assert] cond: all question results were false
--------------------
0 success(es) 1 failure(s) 0 error(s) 1 test(s) run
I can then fix the problem, redefine it (normally, you’d edit the existing definition!):
(: letter-grade2 (-> Integer String))
(define (letter-grade2 n) (cond [(>= n 90) "A"] [(>= n 80) "B"] [(>= n 70) "C"] [(>= n 60) "D"] [else "F"]))
And confirm this works:
(check-contract letter-grade2) 1 success(es) 0 failure(s) 0 error(s) 1 test(s) run
But, we can actually use this mechanism to do something quite a bit more powerful. Notice that one of our built-in atomic contracts is for True: i.e., just the value #t. That might have seemed silly, but it can be combined with check-contract to search for counter-examples for properties about our code!
e.g., our letter-grade2 function just has, as a signature, that it returns a String. Later, we’ll show how to write down richer signatures (for enumerations and itemizations), but for now, we can express, as a property, that letter-grade2 should only return a certain set of string:
(: letter-grade2-prop (-> Integer True)) (define (letter-grade2-prop n) (let ([l (letter-grade2 n)]) (member? l (list "A" "B" "C" "D" "F")))) (check-contract letter-grade2-prop) 1 success(es) 0 failure(s) 0 error(s) 1 test(s) run
What this says is that the output of letter-grade2 had better be in that enumeration.
Exercise: If you write a correct version of my-abs, it should satisfy the contract (-> Integer Natural). However, we’d like you to write a property that captures, more accurately, how an absolute value function should work. e.g., the following satisfies the signature, but is not an absolute value function:
(: my-abs2 (-> Integer Natural)) (define (my-abs2 n) 0) (check-contract my-abs2) 1 success(es) 0 failure(s) 0 error(s) 1 test(s) run
Your property, my-abs-prop, should check that the number my-abs returns is indeed the absolute value of the input. You can start by making sure it works on non-negative input, and then improve it to also ensure the function is correct on negative input as well.