Lecture 6: Design / Specification Recipe🔗

1 Purpose🔗

Introduce design / specification recipe.

2 Outline🔗

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.

Case Study: Color to Black and White

We will now demonstrate our new design recipe via developing a function color->b&w to convert colors to black & white values.

First, we need to define what we mean by a color. We’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))

What have we written here? Our specification says that for any color, we want its luminance to be at least MIN-DELTA away from all the other colors. We want this to be true for any color we are using, so we define the signature of color->b&w-prop to be the contract (-> Color True). This will ensure that no matter which color we are using, it will be distiguishable from all other colors after being converted to monochrome.

After writing a signature, purpose, and specification, we can now implement the function. 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 the implementation still meets the spec!

Exercise: change color->b&w, see if it now fails verification

Exercise: create a test color->b&w-prop-2 that takes two colors, and checks that the colors are either the same, or far enough apart in luminosity. What should its contract be?