Lecture 16: Specification and Implementation.

Is the implementation of the acceptor from the previous lecture really sound? We will see how difficult it is to write a programming that behaves according to specification. We will cast a little light on the questions related to specifications, implementations, and correctness.

The main result of this lecture is that we examine a fix of a problem presented in the previous lecture. .

Suggested Reading Materials:

Robert Harper. Functional Pearls. Proof-Directed Debugging. Journal of Functional Programming, ????

Previous lecture: Lecture 15
Next lecture: Lecture 17