Coursework 1

Question 1

(1)

1. Assume $x,y=100$, values after execution: $\text{do }(!x-1)\text{ times }y:=!y+1$ $\text{do }(99)\text{ times }y:=!y+1$ $x$ is not mutated $y=100+99$ Hence, $x=100,y=199$.
2. Assume $x=0,y=100$. $\text{do }(!x-1)\text{ times }y:=!y+1$ $\text{do }(-1)\text{ times }y:=!y+1$ is divergent The program will infinitely decrement $y$

(2)

counter := !x - 1
while ¬(counter = 0) do (
	y := !y + 1
	counter := !counter - 1
)

Since the original program does not mutate $x$ during execution, we must take care to copy it to a new memory location before continuing. Then we replicate the same loop which executes $x-1$ times, adding $1$ to $y$ each time.

Question 2

(1)

$C::=\dots |\text{ case }L\text{ empty: }{C}_1\text{ nonempty: }{C}_2$

$$\begin{array}{rlrl}⟨(\text{case }L\text{ empty: }{C}_1\text{ nonempty: }{C}_2)\cdot c,r,m⟩& \to ⟨L\cdot \text{case}\cdot c,C_1\cdot C_2\cdot r,m⟩& & \\ & & & \\ ⟨\text{L}\cdot c,r,m⟩& \to ⟨c,\text{True}\cdot r,m⟩& & \text{if }L=nil\\ ⟨\text{L}\cdot c,r,m⟩& \to ⟨c,\text{False}\cdot r,m⟩& & \text{if }L\ne nil\\ & & & \\ ⟨\text{case}\cdot c,\text{True}\cdot C_1\cdot C_2\cdot r,m⟩& \to ⟨C_1\cdot c,r,m⟩& & \\ ⟨\text{case}\cdot c,\text{False}\cdot C_1\cdot C_2\cdot r,m⟩& \to ⟨C_2\cdot c,r,m⟩& & \end{array}$$

(1)

Note: $nil$ indicates the end of the list, however $\text{nil}$ is a variant of $L$.

Let’s assume we start with the configuration as follows: $⟨(\text{case }\text{nil}\text{ empty: }{C}_1\text{ nonempty: }{C}_2)\cdot nil,nil,nil⟩$ Apply the first rule: $⟨(\text{case }\text{nil}\text{ empty: }{C}_1\text{ nonempty: }{C}_2)\cdot nil,nil,nil⟩\to ⟨\text{nil}\cdot \text{case}\cdot nil,C_1\cdot C_2\cdot nil,nil⟩$ As $L=nil$, we apply the first rule of the second set of rules: $⟨\text{nil}\cdot \text{case}\cdot nil,C_1\cdot C_2\cdot nil,nil⟩\to ⟨\text{case}\cdot nil,\text{True}\cdot C_1\cdot C_2\cdot nil,nil⟩$ This matches the first rule of the third set of rules: $⟨\text{case}\cdot nil,\text{True}\cdot C_1\cdot C_2\cdot nil,nil⟩\to ⟨C_1\cdot nil,nil,nil⟩$ This is identical to the machine code generated for $C_1$ which would be just $C_1$ as above.