CS 245 — Lecture 22

Arrays

You may have noticed that one of our examples from the previous lecture used arrays. First, what is an array?

Definition 22.1. Let $A$ be an array of $n$ integers A[0],A[1],...,A[n-1].

Example 22.2. If we just read from arrays, nothing really changes and we can treat expressions as we did before.

In order to solve this, we treat arrays similarly to how we treated environments: by defining the assignment as a re-mapping of the array mapping at the specified index.

Definition 22.3. We define the array $A$ with $A[i]$ assigned to $e$ by $$ A\{i \leftarrow e\}[j] = \begin{cases} e & \text{if $j = i$,} \\ A[j] & \text{if $j \neq i$.} \end{cases}$$ Then we can define the array assignment rule by $$\frac{\quad}{\llparenthesis \psi[A\{e_1 \leftarrow e_2\}/A] \rrparenthesis A[e_1] = e_2 \llparenthesis \psi \rrparenthesis} \text{(array assignment)}.$$

Just like with environments, we have to interpret the array reassignment as an entirely new array, with the change in mapping.

Example 22.4. We will prove the following sequence of assignments.

This should be straightforward if we are careful and follow all of the required substitutions. The only thing that is not immediately clear is how to prove our implication at the top. For that, we'll need a lemma.

Lemma 22.5. Let $A$ be an array and $x,y$ be integers. Then

1. $A\{x \leftarrow A[y]\}\{y \leftarrow A[x]\}[x] = A[y]$, and
2. $A\{x \leftarrow A[y]\}\{y \leftarrow A[x]\}[y] = A[x]$.

First, it's important to get the notation straight before moving on: what exactly is the array $A\{x \leftarrow A[y]\}\{y \leftarrow A[x]\}$? An easy mistake to make is thinking that $$A\{x \leftarrow A[y]\}\{y \leftarrow A[x]\}[y] = A[y]$$ which would make the lemma incorrect. The immediate reasoning is this: since we first assign $A[x] = A[y]$, then it seems like we are changing $A[y]$ to be $A[x]$, which is currently $A[y]$. However, this is incorrect.

We must always remember that $A$ and $A\{x \leftarrow A[y]\}$ and $A\{x \leftarrow A[y]\}\{y \leftarrow A[x]\}$ are all different arrays. What this means is that when we use the notation $\{y \leftarrow A[x]\}$ in the second redefinition of the array, we are assigning index $y$ to the original $A[x]$. To express what we intuitively but incorrectly assumed, we would have to refer to the array $$A\{x \leftarrow A[y]\}\{y \leftarrow A\{x \leftarrow A[y]\}[x]\}$$

Proof. By definition, we have $$A\{x \leftarrow A[y]\}\{y \leftarrow A[x]\}[j] = \begin{cases} A[x] & \text{if $y = j$,} \\ A\{x \leftarrow A[y]\}[j] & \text{if $y \neq j$.} \end{cases}$$

So if $j = y$, we have $A[x]$. If $j = x$, we have $A[y]$ by applying the definition again on $A\{x \leftarrow A[y]\}$. And if $j \neq x,y$, we have $$A\{x \leftarrow A[y]\}\{y \leftarrow A[x]\}[j] = A[j].$$ $$\tag*{$\Box$}$$

Now, our implication follows directly from the lemma. Since there are no loops, our program terminates and we can conclude that our Hoare triple is satisfied under total correctness.

Example 22.6. We will consider a program that reverses an array $R$ by exchanging $R[j]$ with $R[n-1-j]$ for $0 \leq j \leq \left\lfloor \frac n 2 \right\rfloor - 1$. We will prove

j = 0;
while (2*j <= n-2) {
    t = R[j];
    R[j] = R[n-1-j];
    R[n-1-j] = t;
    j = j+1;
}

Here, we use logical variables $r_i$ to refer to the values of the original $R[i]$.

For our invariant, we need to consider whether or not a swap has occurred at index $x$. If $x \lt j$ or $x \gt n-1-j$, then $R[x]$ and $R[n-1-x]$ have already been swapped. But if $j \leq x \leq n-1-j$, then no swap has happened yet. So we can define $\operatorname{Inv}'(j)$ to be \begin{align*} (\forall x (((0 \leq x \lt j) \rightarrow (R[x] = r_{n-1-x} \wedge R[n-1-x] = r_x)) \\ \wedge ((j \leq x \leq \frac{n-1}2) \rightarrow (R[x] = r_x \wedge R[n-1-x] = r_{n-1-x}))) \end{align*} Then we take our invariant to be $\operatorname{Inv}(j) = \operatorname{Inv}'(j) \wedge (0 \leq j \leq \frac n 2)$. This gives us the following proof.

Observe that the bulk of the work that we do inside the loop is really just the swapping array elements code that we saw in Example 22.4. Now, let's show that our implications hold.

For (a), we have as our premise $$(\forall x ((0 \leq x \leq n-1) \rightarrow (R[x] = r_x)))$$ and we want to conclude $\operatorname{Inv}'(0) \wedge (0 \leq \frac n 2)$, where $\operatorname{Inv}'(0)$ is defined \begin{align*} (\forall x (((0 \leq x \lt 0) \rightarrow (R[x] = r_{n-1-x} \wedge R[n-1-x] = r_x)) \\ \wedge ((0 \leq x \leq \frac{n-1}2) \rightarrow (R[x] = r_x \wedge R[n-1-x] = r_{n-1-x}))) \end{align*} We can simplify $\operatorname{Inv}'(0)$ by observing that $0 \leq x \lt 0$ is always false and so the first portion of the conjunction always evaluates to true. Then we must consider $$((0 \leq x \leq \frac{n-1}2) \rightarrow (R[x] = r_x \wedge R[n-1-x] = r_{n-1-x})).$$ Observe that this simply says that every element $R[x] = r_x$, which is exactly the statement of our premise.

We can show (b) similarly but we now need to deal with $x = j$. We begin by observing that $((j \leq \frac n 2) \wedge (2 \cdot j \leq n - 2))$ implies $j+1 \leq \frac n 2$. Another key observation is the fact that by definition, we have that $R$ and $R' = R\{j \leftarrow R[n-1-j]\}\{(n-1-j) \leftarrow R[j]\}$ are identical except at indices $j$ and $n-1-j$.

Then for $x = j$, in our premise, we have $(R[j] = r_j) \wedge (R[n-1-j] = r_{n-1-j})$ but in our conclusion we have $(R'[j] = r_{n-1-j}) \wedge (R[n-1-j] = r_j)$. By definition of $R'$ we have $R'[j] = R[n-1-j] = r_{n-1-j}$ and $R'[n-1-j] = R[j] = r_j$, as required.

Finally, to show (c), recall that we have $\operatorname{Inv}'(j)$ defined by \begin{align*} (\forall x (((0 \leq x \lt j) \rightarrow (R[x] = r_{n-1-x} \wedge R[n-1-x] = r_x)) \\ \wedge ((j \leq x \leq \frac{n-1}2) \rightarrow (R[x] = r_x \wedge R[n-1-x] = r_{n-1-x}))) \end{align*} Suppose $n$ is even. Then $\frac n 2$ is an integer and we have $((j \leq \frac n 2) \wedge (2 \cdot j \gt n-2))$ gives $j = \frac n 2$. This gives us \begin{align*} (\forall x (((0 \leq x \lt \frac n 2) \rightarrow (R[x] = r_{n-1-x} \wedge R[n-1-x] = r_x)) \\ \wedge ((\frac n 2 \leq x \leq \frac{n-1}2) \rightarrow (R[x] = r_x \wedge R[n-1-x] = r_{n-1-x}))) \end{align*} Observe that $\frac n 2 \leq x \leq \frac{n-1}2$ is always false, so we are left with $((0 \leq x \lt \frac n 2) \rightarrow (R[x] = r_{n-1-x} \wedge R[n-1-x] = r_x))$ which says that every element has been appropriately swapped.

Similarly, if $n$ is odd, we have that $((j \leq \frac n 2) \wedge (2 \cdot j \gt n-2))$ gives $j = \frac{n-1} 2$. This gives us \begin{align*} (\forall x (((0 \leq x \lt \frac{n-1}2) \rightarrow (R[x] = r_{n-1-x} \wedge R[n-1-x] = r_x)) \\ \wedge ((\frac{n-1}2 \leq x \leq \frac{n-1}2) \rightarrow (R[x] = r_x \wedge R[n-1-x] = r_{n-1-x}))) \end{align*} which when simplified gives us $((0 \leq x \lt \frac{n-1} 2) \rightarrow (R[x] = r_{n-1-x} \wedge R[n-1-x] = r_x))$ which again says that every element has been appropriately swapped.

To prove that this program terminates for satisfaction under total correctness, we would take the loop variant to be $\left\lfloor \frac n 2 \right\rfloor - j$.