CSC 208-01 (Spring 2023)

Lab: Introduction to Algorithmic Verification

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:

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:

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.

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\).

  1. Proof the Knight’s Walks claim by induction on the size of the chessboard.

  2. 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.

  3. 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!

  4. 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.

  1. 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.

  2. Suppose that \(s = 4\). Argue in a sentence or two why the first player does not have a winning strategy.

  3. 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.

  4. Suppose that \(s = 8\). Argue in a sentence or two why the first player does not have a winning strategy.

  5. 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\).)