Executional abstraction; The role of programming languages; States and their characterization; The characterization of semantics; The semantic characterization of a programming language; Two theorems; On the design of properly terminating; Euclid's algorithm revisited; The formal treatment of some small examples; The linear search theorem; The problem of the next permutation.

As I have now said many times and written in many places: program testing can be quite effective for showing the presence of bugs, but is hopelessly inadequate for showing their absence.