Chapter 3
Reasoning about programs
Aims

To show how properties of functions and other Miranda objects can be
proved using elementary techniques of logic.
 In particular, the
chapter introduces proof by induction
over the natural numbers; `mathematical
induction' in other words.
Issues
Relevance
It is an
important fact that functional programs are more amenable to verification than
most imperative programs, and it is therefore somewhat simpler to introduce
verification in a functional setting.
The thread on proof through the book can be treated as optional, but it has
been included as an integral part of the text because I see it as central to
learning functional programming.
Strategies for teaching proof
Proof is hard to teach; the ground rules for writing proofs are less clearly
defined than for a programming language, and induction in particular looks
circular to many students. There seems to be no `silverbullet' explanation,
but a number of ideas help:

Simplification of expressions involving variables works in exactly the same
way as calculation. For the direct proofs at the start of the chapter, this is
really all that is needed.

Induction is like recursion. A familiarity with recursive definitions, and
the conviction that they work, can help in convincing students that induction
is not circular. The view of the proof as a machine turning proofs into proofs
can also help.

Proving the induction step involves making an assumption; examining particular
examples of chains of reasoning involving real world assumptions can
convince that they are different than proofs without assumptions.

To tighten up on the mechanics of proof, three points are important:

Keeping the variables in the definition and the proof different makes it
clearer when substitutions in the definition take place.

Providing a template for proofs forces students to be clear about the
subgoals that induction produces; in particular this is helpful when a
formula contains more than one variable.

If the (sub)goal is to prove an equation, a sensible strategy is to
simplify
(like calculation, as above) both sides, and try to get a common result. It is
important to check whether the induction hypothesis has been used, when
appropriate.
Ultimately, there seems to be no substitute for trying examples and getting
constructive feedback on the solutions.
Next
Up
Written 18 May 1995.