Lecture 5: Design / Specification Recipe

1 Purpose

Introduce design / specification recipe.

2 Outline

Another built-in contract In addition to the atomic contracts we saw last time, LSL has built-in support for Lists. Unlike the previous contracts, it takes a parameter, since a List on its own isn’t very meaningful: it has to be a list that contains elements of some type.

We can see this in use with the following example:

(: only-non-negative (-> (List Integer) (List Natural))) (define (only-non-negative lon)   (filter (lambda (n) (or (zero? n) (positive? n))) lon)) (check-contract only-non-negative)

1 success(es) 0 failure(s) 0 error(s) 1 test(s) run

To practice, write a function from a list of integers to a list of booleans, where for each number, you transform it into #t if the number is even? and #f otherwise. Try passing it a list that contains non-integers (e.g., (list 1.1 2 3)), and see what happens if you have a bug in your code so that instead of returning booleans, you return something else.

Design Recipe, Revisited

At this point, we’ve figured out how to express formulas from propositional logic as code, and truth tables as unit tests. We also saw, in the first few days, how we can express purpose statements as code: this was a preview of where we are going, though we will go quite a bit further than that. Let’s get started.

Consider a problem: converting colors to black & white. This comes up, among other places, in accessibility: different people perceive visible light in different ways, and one way of checking if particular sets of colors are likely to still be distinguishable is to convert them to black & white, and check if they are still different, as even people who see colors differently are still likely to distinguish luminance.

In F1, you learned the design recipe:

1. Signature

2. Purpose

3. Tests

4. Implementation

Here, we are going to slightly change the recipe, to emphasize different parts:

1. Signature

2. Purpose

3. Specification / Tests

4. Implementation

5. Verification

In particular, we add the idea of a specification, which will supplement or partly supplant the purpose, and we add a step at the end: verification. That was always an implied step (you run your tests!) but since our tests/specifications will get more interesting, it’s worth emphasizing this step more than has been done. Always, the verification is checking that the implementation matches the specification.

Unit tests are a form of specification, but they are not the only one.

In particular, they are pointwise specifications. They tell us how the function will behave on particular inputs. This may or may not be illuminating: it depends on the function.

Let’s apply this to our color->b&w function.

First, we need to define what we mean by a color. I’ll define it as an enumeration of several options:

; A Color is one of:

;  - "red"

;  - "blue"

;  - "green"

;  - "yellow"

;  - "purple"

(define RED "red")

(define BLUE "blue")

(define GREEN "green")

(define YELLOW "yellow")

(define PURPLE "purple")

(define ALL-COLORS (list RED BLUE GREEN YELLOW PURPLE))

Now, I need a signature, purpose, and specification for my function:

; min-list : [NonEmptyListOf Number] -> Number ; returns the minimum of the list (define (min-list lon)   (apply min lon))   ; color->b&w : Color -> Number[0,255] ; converts a color to its luminance (b&w value) (define MIN-DELTA 20) (define (color->b&w-prop c)   (let* ([LUM (color->b&w c)]          [OTHER-LUM (map color->b&w (filter (lambda (c1) (not (string=? c1 c))) ALL-COLORS))]          [DELTAS (map (lambda (lum) (abs (- LUM lum))) OTHER-LUM)])      (> (min-list DELTAS) 20))) (check-expect (color->b&w-prop RED) #t) (check-expect (color->b&w-prop BLUE) #t) (check-expect (color->b&w-prop GREEN) #t) (check-expect (color->b&w-prop YELLOW) #t) (check-expect (color->b&w-prop PURPLE) #t)

What have I written here? My specification says that for any color, I want its luminance to be at least MIN-DELTA away from all the other colors. I am checking that for all the colors that I am using. This will ensure that no matter the combination of colors, if they are viewed after being converted to black & white, they will still be distinguishable.

I could write my tests in a slightly more compact, and better, way, that wouldn’t rely upon me remembering to add a test when I added a color:

(check-expect (andmap color->b&w-prop ALL-COLORS) #t)

This relies upon the fact that my tests now just return #t when they pass, and I can thus combine them easily using and (or andmap).

What should the implementation be? Well, one option would be to simply assign luminance values to the colors arbitrarily, but if we did that, the results might be confusing: ideally we would like there to be a correspondance to how the colors are percieved by human eyes, so what we will do instead is first match RGB colors to our named colors, and then use a standard conversion that approximates luminance in perception. The intended goal is that if we printed out the color and printed out our converted b&w value, to someone who did not percieve color at all, they should look similar.

(define-struct rgb [R G B]) ; An RGB is a (make-rgb Number[0,255] Number[0,255] Number[0,255]) ; Interpretation: color using standard red, green, blue color values   (define (color->rgb c)   (cond [(string=? c RED) (make-rgb 255 0 0)]         [(string=? c BLUE) (make-rgb 0 0 255)]         [(string=? c GREEN) (make-rgb 0 255 0)]         [(string=? c YELLOW) (make-rgb 255 255 0)]         [(string=? c PURPLE) (make-rgb 255 0 255)]))   (define (color->b&w c)   (let ([rgb (color->rgb c)])     (+ (* 0.299 (rgb-R rgb)) (* 0.587 (rgb-G rgb)) (* 0.114 (rgb-B rgb)))))

Exercise: add another color, see if it fails the spec!