Lecture 2: Logistics, Specifications in LSL
1 Purpose
Cover course policies, start propositional logic.
2 Outline
Introduce yourself to neighbor!
Survey! Must complete this: helps us understand your background, how to tune the class.
Sign up for Discord. IMPORTANT: Must set your display name for the server to your Full Name before we give you access to the course channels. All class communication will go through Discord.
Bring computer to class! We’ll often write things in class.
Install DrRacket, if you don’t have it already. Update it if it’s below 8.11
Install Logical Student Language
You can install it from within DrRacket by going to File -> Package Manager..., and then searching for lsl.
Switch to "Determine Language from Source" at the bottom left (to get this option, you may need to click "Choose language" and then choose "The Racket Language") and begin each file with "#lang lsl".
Documentation for LSL is available at:
https://docs.racket-lang.org/lsl/
This language is (essentially) extension of the the Intermediate Student Language with Lambda (ISL+) language from Fundies 1, with a lot of features for logical reasoning.
If you need review of ISL+ —
If you’d rather watch videos, these are a concise presentation of most of what was in Fundies 1:
https://users.cs.utah.edu/~mflatt/htdp-lite/
We will assume you all know it to the level reached by the end of Fundies 1, so if it has been a while, please do this review.
HW1B is essentially a test of this: if you find it challenging, please spend the time to review.
Syllabus!
Important details: grading allocation, HW collaboration policies, etc.
(covered in some detail)
Office hours
Have already started. Almost all in-person; one (on Saturday) is online. In addition to TAs, I have open drop-in hours (will be Tuesdays, hours TBD: starting next week); you can talk to me about stuff from the class, but also, anything else you are interested in. I’m happy to talk about research, larger implications of any of this, projects you’re working on, etc.
Homework
Twice a week, due Tuesday & Thursday at 9PM . Thursday will be autograded & solo; Tuesday may be autograded or manually graded. If manually graded, we will aim to get the grades back to you by the weekend. Homework in this class is the primary way that you will learn the material, so we want the feedback loop to be tight.
First one is due this Thursday!
Start experimenting with LSL
Set "Determine Language from Source" at bottom left, write #lang lsl at top of file, write some simple functions.
In addition to (most of) the features from ISL+, LSL adds a couple ones. We’ll start, however, using something you should remember from Fundies 1:
(check-expect (f1 10 2) 12) 1 success(es) 0 failure(s) 0 error(s) 1 test(s) run
We’ll learn quite a bit more about testing this semester, and how to go much further than just unit tests, but unit tests will remain useful. One different perspective: if you write predicates (boolean-returning-functions) on the output and use those in your unit tests instead, you can write tests in a slightly different way:
; my-abs : Number -> Number ; takes absolute value of number
(define (my-abs x) (if (< x 0) (* x -1) x)) ; nonnegative? : Number -> Boolean
(define (nonnegative? x) (or (= x 0) (positive? x)))
(check-satisfied (my-abs 10) nonnegative?) (check-satisfied (my-abs -5) nonnegative?) (check-satisfied (my-abs 0) nonnegative?) 3 success(es) 0 failure(s) 0 error(s) 3 test(s) run
check-satisfied is in ISL+, though you may not have used it. This snippet of code, simple as it is, is our first example of a formal specification. What we are expressing, formally, is that the result of my-abs should be non-negative.
It is formal because it is expressed in unambiguous language: in this case, in executable LSL code. And it is a specification because it is an abstracted, higher level description of the behavior of the program. Hopefully, that has utility to someone who wants to use or understand the code. Purpose statements, what you are familiar with, are informal specifications: they similarly convey meaning to people who want to use or understand the code, but they are informal because they lack precision.
Why do you think we prefer formal to informal specifications?
Answer: precision is useful, but can come at a cost of complexity. But, the benefit is that we can often actually connect them to the code we run, as above. Not only are we expressing that the result should be non-negative, we are validating that on a set of inputs.
Now, we could have written the above as typical unit tests instead:
(check-expect (my-abs 10) 10) (check-expect (my-abs -5) 5) (check-expect (my-abs 0) 0) 3 success(es) 0 failure(s) 0 error(s) 3 test(s) run
What do we lose? Nowhere do we indicate that we intend that the output is always nonnegative.
Perhaps a reader would understand from the behavior that this is what is going on, and an informal specification (a purpose statement) would go a long way to helping. Another advantage of expressing the property we wish to hold in executable form is that if the reader is skeptical of our set of tests (i.e., they wonder if our property holds of the input -42), they can easily add that test:
(check-satisfied (my-abs -42) nonnegative?) 1 success(es) 0 failure(s) 0 error(s) 1 test(s) run
That’s not the case with just unit tests, as they need to figure out what should the function return on input -42 before they can write that test. Hopefully the informal specification (purpose statement) allows them to determine that, but that relies upon the purpose statement being really really clear.
There are also functions we can write where unit tests can’t even accurately specify the behavior. Let’s see an example:
; prime-factor-of : Number -> Number ; returns one of the prime factors of the input number. (define (prime-factor-of n) ...)
I’ve deliberately left out the implementation, because there is a problem when we go to write tests:
(check-expect (prime-factor-of 3) 3) (check-expect (prime-factor-of 7) 7) ; (check-expect (prime-factor-of 10) 2) ; (check-expect (prime-factor-of 10) 5)
The last two have different outputs, but the same input! Which is not something a function can do! We could choose one, but then we are overly specifying the behavior of our function. It may seem simple to specify that it should return the smallest prime factor, but what if someone comes up with a clever algorithm that may return some other factor? If we specified, in the form of unit tests, that it had to return the smallest, it would be wrong.
Why would we want such a function? Well, we could use it to build a primality tester:
; prime? : Number -> Boolean (define (prime? n) (= (prime-factor-of n) n))
And in general, we often have problems that can be solved in many different ways. We could opt to just never test our function on non-prime numbers, but that would be pretty terrible, as an implementation that just returned its input would pass that set of tests.
We can, and should, do better:
(define (prime-factor-of-prop n) (let ([factor (prime-factor-of n)] [divides? (lambda (x y) (= (remainder y x) 0))]) (and (divides? factor n) (andmap (lambda (x) (not (divides? x factor))) (range 2 (sub1 factor) 1)))))
Now, we’ve expressed exactly what we mean by "prime factor of": first, that it is a factor (in that it divides the input), and second, that it is prime (via an inefficient algorithm). Now, no matter how prime-factor-of is defined, provided it is correct, it should pass this specification. We can thus write tests using it, rather than as unit tests:
(check-expect (prime-factor-of-prop 3) #t) (check-expect (prime-factor-of-prop 7) #t) (check-expect (prime-factor-of-prop 10) #t)
Note that we wrote this specification slightly differently than we did the one for my-abs: this time, the assertions about the output depend on the input in a fundamental way.
Stepping back we will see lots of ways to write specifications this semester, and lots of ways to connect them to code, but the general pattern you already see will carry through all of it. The point of formal specification is to be precise (more precise than a purpose statement) and to be able to actually validate your specification.