Reasoning: An Introduction to Logic, Sets, and Functions

Subsection 6.2.9 Specifications for the Tower of Hanoi Problem

How shall we write logical expressions that correspond to the specification for a program to solve the Towers of Hanoi problem?

A useful way to do this is to write three things:

• A precondition: What is guaranteed to be true when the program starts?

• A postcondition: What must be true when the program finishes in order for it to have performed correctly?

• One or more invariants: Claims that can be shown to be true all along as the program runs. The point of stating such invariants is to make it possible to prove that, if the precondition holds when the program begins, the postcondition will hold when it ends. So we want to capture key facts about the problem and its solution.

For this problem, in order to do this we’ll need the following predicates:

Disk(x): True if x is a disk.

Pole(x): True if x is a pole.

On(x, y, t): True if x is on y at time t.

Above(x, y, t): True if x is above y on some pole at time t.

LargerThan(x, y): True if x is larger than y.

We’ll assume that all the disks start out on Pole1 and should end up on Pole3.

Let’s first define the precondition (i.e., what’s true when we start):

∀x (Disk(x) → On(x, Pole1, time1)) At time 1, every disk is on Pole1.

Now let’s define conditions that must always be true (except when we are in the middle of a single move). In other words, these conditions will be true when we start, they’ll be true when we finish, and they must be maintained by each move as we are in the process of solving the puzzle. We call such conditions invariants because they never change during the solution process. Notice that we could include here such claims as “The Earth revolves around the Sun.” It’s an invariant. But it won’t help us reason about a solution to this problem. Doing that requires encoding two key facts:

1. At each step, every disk is on some pole.

2. At each step, given any disk, any disks below it are bigger than it is.

Here we’ve written a single claim that is the conjunction of those two:

∀t (∀x, y ((Disk(x) ∧ Disk(y) ∧ Above(x, y, t)) → LargerThan(y, x))) At all times t, if disk x is

above disk y, y is larger

than x.

∧

∀t, x (Disk(x) → ∃y (Pole(y) ∧ On(x, y, t))) At all times, every disk must be on

some pole.

Finally, we must describe the postcondition (i.e., what must be true when we finish): We’ll leave this for you to figure out as an exercise.