So far in this course, we’ve used program verification as a means to
motivate the mathematical foundations of computing. We will now
transition from program verification to *algorithmic
verification* where we are interested in verifying properties of
algorithms *independent* of the language they are stated in.
While the latter can be thought of the former—whatever language we state
an algorithm is a “programming” language of some sort—it is important to
distinguish the two kinds of verification. In particular, while program
verification is usually backed by some kind of formal model of the
implementing programming language, algorithmic verification does not
usually feature such a model. Instead, we rely on our intuition in
tandem, the rules of mathematical logic, and any other mathematical
formalisms we employ to verify algorithms. This makes algorithmic
verification feel more arbitrary and ad hoc, but the benefit is that we
can now reason about things independent of our choice of programming
language!

In tandem, one thing that stays consistent between program and
algorithmic verification is the coupling of *design* and
*verification*. We emphasized the idea that the reasoning we
employed in program verification mimicked the design of our program. For
example, if our code contained a conditional, we reasoning about the
*cases* induced by that conditional, *i.e.*, its if-branch
and else-branch. There are two perspectives on this kind of
reasoning:

- The
*verification*perspective is that if we want to ensure that a property holds of a conditional, it is sufficient to verify that condition in each branch independently. In each branch, we assume the guard of the conditional is true and false, respectively. - The
*design*perspective is that if we are designing a conditional that should have a property hold of it, it is sufficient to design its branches independently. When designing each branch, we assume the guard of the conditional is true and false, respectively.

Observe how verification and design are two sides of the same coin—we can’t help perform one task without thinking about the other! In today’s lab, we’ll take a look at our first problem in this space of algorithmic verification and see how verification is related to design.

# Problem: Constructive Thoughts

Chess is played on a \(n \times n\) board (with \(n = 8\)) usually). There are a variety of pieces in chess, each of which move in a different way. For these claims, we will consider two pieces:

- The
*rook*which can move any number of squares in a cardinal (non-diagonal) direction. - The
*knight*which moves in a L-shaped pattern: 2 squares horizontally, 1 square vertically or 2 squares vertically, 1 square horizontally.

Furthermore, we will consider two problems (really, thought experiments because these specific situations never arise in a real chess game) when only one such piece is on the board.

- The
*walk*is a sequence of moves for this single piece that causes the piece to visit*every*square of the board. - A
*tour*is a*walk*with the additional property that the piece visits every square*exactly once*.

When considering walks and tours, we are free to initially place our piece on the board at any position. In addition, we only consider a square visited if the piece ends its movement on that square. Putting it all together, here are the two claims that we will consider and ultimately prove:

**Claim: (Knight’s Walks)**. There exists a knight’s
walk for any chessboard of size \(n \geq
4\).

**Claim (Rook’s Tours)**. There exists a rook’s tour for
any chessboard of size \(n \geq
1\).

Proof the

**Knight’s Walks**claim by induction on the size of the chessboard.From your proof, describe an

*algorithm*for performing a Knight’s walk on an \(n \times n\) chessboard with \(n \geq 4\). Because your proof is inductive, your algorithm should be recursive, following the structure of your proof.Next, describe an algorithm for performing a Rook’s tour on an \(n \times n\) chessboard of size \(n \geq 1\). Try to describe it recursively, similarly to your proof/algorithm for the Knight’s walk.

(

*Hint*: be mindful of how an \(n \times n\) chessboard grows to an \((n+1) \times (n+1)\) chessboard. How does our recursive algorithm account for this growth? It is more complicated that it looks at first glance!Finally, translate your Rook’s tour algorithm into a proof of the Rook’s Tour claim by induction on the dimensions of the chessboard.

# Problem: Take It Away

In variations of *take-away* games, two players take turns
removing objects from a pile. The allowable number of objects that a
player can remove in their turn is a finite, fixed set of amounts,
*e.g.*, a player can only remove one, two, or three objects on
their turn. The winner of the game is the one to remove the last object
from the pile.

For our analysis, we will assume that the pile contains \(s\) objects and players may remove \(1\), \(2\), or \(3\) objects at a time although we can generalize our result to a pile of \(n\) objects with \(\{\, k_1, \ldots, k_m \,\}\), \(m\) different choices of amounts to remove from the pile.

Suppose that \(1 \leq s \leq 3\). Describe a winning strategy that the first player can execute to win the game. A winning strategy is a collection of rules for choosing how many objects to remove from the pile.

Suppose that \(s = 4\). Argue in a sentence or two why the first player

*does not*have a winning strategy.Suppose that \(5 \leq s \leq 7\). Describe a winning strategy for the first player. This strategy should account for any choices that the second player makes.

Suppose that \(s = 8\). Argue in a sentence or two why the first player

*does not*have a winning strategy.Finally, based on your analysis, fill in the following claim:

**Claim**: suppose that we are playing a take-away game with a pile containing \(s\) objects and players can remove \(1\), \(2\), or \(3\) objects at a time. If the following property about \(s\) is true \(\ldots\) then player one always has a winning strategy.Prove this claim by giving a winning strategy for player one in this scenario.

(

*Hint*: proceed by induction on the size of the pile. In doing this induction, you will need to employ*strong induction*where your induction hypothesis holds not just for \(n-1\) but for any \(k < n\).)