Lecture 4: Design / Specification Recipe

1 Purpose

Introduce design / specification recipe.

2 Outline

At this point, we’ve figured out how to express formulas from propositional logic as code, and truth tables as unit tests. What we will do is figure out how to apply these ideas to programs!

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 thing, 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. Running our tests was always this step, but since running tests is easy, we didn’t distinguish between that and the implementation step. As we’ll see throughout the semester, sometimes verification is indeed quite a lot of work, above and beyond the implementation. Always, the verification is checking that the implementation matches the specification. Further, tests are a form of specification.

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:

; 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)
  (local [(define LUM (color->b&w c))
          (define OTHER-LUM (map color->b&w (filter (lambda (c1) (not (string=? c1 c))) ALL-COLORS)))
          (define DELTAS (map (lambda (lum) (abs (- LUM lum))) OTHER-LUM))]
     (> (foldr min 255 DELTAS) 20)))
(check-property (color->b&w-prop RED))
(check-property (color->b&w-prop BLUE))
(check-property (color->b&w-prop GREEN))
(check-property (color->b&w-prop YELLOW))
(check-property (color->b&w-prop PURPLE))

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.

What should the code be? Well, one option would be to simply assign luminance values to the colors, but ideally, it has some correspondance to how the colors are viewed, so what we will do instead is first match RGB colors to our named colors, and then use a standard conversion that approximates perception.

(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)
  (local [(define 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!