\dbox{{\bf Deliverable:} Submit your responses as a single, readable PDF file on the collab site before {\bf 6:29pm} on {\bf Friday, 20 October}. The PDF you submit can be a scanned handwritten file (please check the scan is readable), or a typeset PDF file (e.g., generated by LaTeX).}

Directions

Solve as many of the 8 problems as you can. For maximum credit, your answers should be correct, clear, well-written, and convincing.

Problems marked with $(\star)$ are challenging enough that it is not necessary to solve them well to get a ``gold-star level” grade on this assignment (although we certainly hope you will try and some will succeed!)

State Machines

1. Describe a state machine that can be used to determine if the number of steps is divisible by 3. You should clearly define the set of states in your machine, and how each is interpreted, and the transition relation. (Don’t forget to also specify $q_0$.)

2. Describe the set of states that are reachable for the ``Progress” Machine defined as $M = (S, G, q_0)$:

   $S = { (x, d) \, | \, x \in \mathbb{Z}, d \in { \mathrm{\bf F}, \mathrm{\bf B}} }$
   $G = { (x, \mathrm{\bf F}) \rightarrow (x + 1, \mathrm{\bf B}) \, | \, x \in \mathbb{Z} } \cup { (x, \mathrm{\bf B}) \rightarrow (x - 2, \mathrm{\bf F}) \, | \, x \in \mathbb{Z} }$
   $q_0 = (0, \mathrm{\bf F})$

3. $M = (S, G \subseteq S \times S, q_0 \in S)$ is a state machine where the cardinality of $S$ is finite, and transition relation, $G$, is a total injective function. Show that it is possible for some states in $S$ to be unreachable.

Knight’s Moves

1. ($\star$) A knight in chess can move two squares up, down, left, or right, followed by one square in a direction perpendicular to the two squares (so, it can move two squares up or down, followed by one square left or right; or, can move two squares left or right, followed by one square up or down). We can define the possible moves of a knight on an infinite chess board as the Knight State Machine (similarly to how we defined the Bishop State Machine in Class 14):

   $S = { (r, c) \, | \, r, c \in \mathbb{N} }$ $G = { (r, c) \rightarrow (r’, c’) \, | \, r, c \in \mathbb{N} \wedge ((r’ = r \pm 2 \wedge c’ = c \pm 1) \vee (r’ = r \pm 1 \wedge c’ = c \pm 2)) \wedge r’ \ge 0 \wedge c’ \ge 0 }$ $q_0 = (0, 0)$

   Prove that all states in $S$ are reachable for the Knight State Machine. (Hint: use induction, but be careful to either set up an appropriate $P(n)$ or break the proof into two separate induction proofs to show you can reach any column and can reach any rwo.)

Invariant Principle

1. MCS Problem 6.3.

2. Use the principle of induction to prove the invariant principle. (Hint: your induction predicate, $P(n)$ should use $n$ as the number of steps.)

3. MCS Problem 6.11. Parts (b) and © are considered ($\star$)-ed parts. For part (a) you can only list the items that are preserved invariants, but for part (b) and © your answers should contain full proofs for any claims or answers (even for part (b) where the wording of the problem in the book asks for only a number).

There is also some typos in how the part (a) is listd. The actual (simpler-to-solve) peroperties are as follows. $rem(a,b)$ is the remainder of dividing $a$ by $b$ and is the same as $a \mod b$.

(6.5) $rem(n_b+n_w, 3) \neq 2$

(6.6) $rem(n_w-n_b, 3) = 2$

(6.7) $rem(n_b-n_w, 3) = 2$

(6.8) $n_b + n_w > 5$

(6.9) $n_b + n_w < 5$

1. ($\star$) Prove the Python program below is a correct implementation of the factorial function.

   def factorial(n):
       x = 1 # poor choices of variable names for programmers
       y = 1 
       while x <= n:
           y = y * x
           x = x + 1
       return y
   

   To be correct, for any input $n \in \mathbb{N}$, the program should always return a result equal to $n!$. The factorial of $n$ is defined as the product of all positive integers up to and including $n$. (Note that $0! = 1$.)

   A good answer will explain (1) how to map the program to a state machine, (2) come up with a preserved invariant property that (2.a) holds at the beginning and (2.b) if it holds at the termination, it implies the right answer is produced. A perfect answer also shall argue why the program terminates.