In this videotape, Dijkstra gives a tutorial on program verification. He uses two toy examples, in which he develops the program and its proof at the same time. The material covers basic concepts of assertions, invariants, pre-conditions, post-conditions, partial correctness, total correctness, and Hoare proof rules for loops.

The material is neither introductory (for example, knowledge of simple logical connectives and nondeterministic guarded commands is essential) nor advanced (only short sequential programs are discussed). The lecture is well-planned and delivered with the minimum of video effects. In fact, the greatest value of this videotape is the opportunity to experience one of the early pioneers of program verification speaking on his favorite subject.