Lecture 2: Logistics, Specifications in ISL
1 Purpose
Cover course policies, start propositional logic.
2 Outline
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.6
Install ISL-Spec
You can install it from within DrRacket by going to File -> Install Package..., and then searching for isl-spec.
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 isl-spec".
This language is an extension of the the Intermediate Student Language with Lambda (ISL+) language Fundies 1, with a few features for logical reasoning.
If you need review of ISL+:
We’ll also, twice during the semester, install additional pieces of software, but we’ll defer until we need them.
Quizes Will happen nearly every day. They are short, and we will drop about the lowest 1/3 of them, so if you are sick, or miss a few classes, you won’t be penalized. They happen via PollEverywhere, which you should log in to now, using your phone:
pollev.com/logic
Let’s try doing one: this one doesn’t count, but confirms that you’re able to take them.
Syllabus!
Important details: grading allocation, HW collaboration policies, in-class quizes.
(cover in some detail)
Office hours
Start next week. Most are online, but some are in-person. In addition to TAs, I have open drop-in hours; 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
Due every week, Wednesdays at 6pm. We will aim to get them 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.
Start experimenting with isl-spec
Set "Determine Language from Source" at bottom left, write #lang isl-spec at top of file, write some simple functions.
; f1 : Number Number -> Number
; adds two numbers
(define (f1 x y)
(+ x y))
In addition to all the features from ISL+, ISL-Spec adds a few new ones. The first is that we have a new check-property that has two ways of using it. First is, it takes an expression that returns a boolean and ensures that it is true. i.e.,
(check-property (= (f1 10 2) 12))
But that could have been better written as:
(check-expect (f1 10 2) 12)
What we actually will use it for is to write down predicates that we expect to hold, and then use check-property with them. For example:
; 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-property (nonnegative? (my-abs 10)))
(check-property (nonnegative? (my-abs -5)))
(check-property (nonnegative? (my-abs 0)))
This is our first example of a formal specification: the result of my-abs should be non-negative. It is formal because it is expressed in unambiguous language: in this case, in executable ISL-Spec code. And it is a specification because it is an abstracted, higher level description of the behavior of the program, that hopefully has utility to someone who wants to use or understand the code. Purpose statements, with you are familiar with, are informal specifications.
Why do you think we prefer formal to informal specifications?
Answer: better precision, and we can often actually connect them to the code we run, as above.
Now, we could have written the above as unit tests instead, albeit while losing the informative observation that the output is nonnegative.
(check-expect (my-abs 10) 10)
(check-expect (my-abs -5) 5)
(check-expect (my-abs 0) 0)
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. But there are plenty of functions we can write where unit tests can’t even accurately specify the behavior. Let’s see an example:
; longest-string : [List-of String] -> String
; returns longest string in list or "" if empty
(define (longest-string los) ...)
(check-expect (longest-string (list "a" "bb" "CCC")) "CCC")
(check-expect (longest-string (list)) "")
;(check-expect (longest-string (list "aa" "b" "c" "dd")) "aa")
;(check-expect (longest-string (list "aa" "b" "c" "dd")) "dd")
I’ve deliberately left out the implementation, because there is a problem with the tests: the last two have different outputs, but the same inputs! Which is not something a function can do! We could choose one, but then we are overly specifying the behavior of our function: we are saying it has to return the first longest or the last longest What if someone comes up with a clever algorithm that will return one of the longest, but not necessarily that one: according to our specification, in the form of our tests, it would be wrong.
We can, and should, do better:
(define (longest-string-prop l)
(let [(max-len (string-length (longest-string l)))]
(andmap (λ(s) (<= (string-length s) max-len)) l)))
(check-property (longest-string-prop (list "aa" "b" "c" "dd")))
Now, we’ve expressed exactly what we mean by longest string, in a formal specification: that the lengths of all the strings in the list are at least as big as it! This means that we could define longest-string with, for example, either foldr or foldl and all of the tests would still pass: something that would have been impossible before, unless we simply didn’t test any cases where there were multiple strings with the longest length (which would be pretty terrible).
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.