def sort(L):
'''
Precondition:
L is a list of 0s and 1s
Postcondition:
L is sorted (non-descending)
Returns True if 0 in L and False otherwise
'''
i = 0
j = -1
while i < len(L):
if L[i] == 0:
j += 1
L[i], L[j] = L[j], L[i]
i += 1
return j >= 0


Let $$\mathbb{N}$$ be the set of nonnegative integers. For $$a,b \in \mathbb{N}$$, define

$\mathtt{range}(a,b) = \{x \in \mathbb{N} : a \leq x < b\}$

If $$a \geq b$$, then $$\mathtt{range}(a,b)=\emptyset$$.

If $$a < b$$, then $$\mathtt{range}(a,b)=\{a,\ldots,b-1\}$$, e.g. $$\mathtt{range}(0,4)=\{0,1,2,3\}$$.

Define the predicate $$P(i,j)$$ by

1. $$-1 \leq j < i \leq \mathtt{len}(L)$$.
2. If $$x \in \mathtt{range}(0,j+1)$$, then $$L[x]=0$$.
3. If $$x \in \mathtt{range}(j+1,i)$$, then $$L[x]=1$$.

# If list $$L$$ is empty

## Entering loop

$$P(0,-1)$$ is true because $$\mathtt{range}(0,0)=\emptyset$$.

## Executing loop

The loop does not execute.

## Exiting loop

Suppose that $$P(i,j)$$ is true when the loop exits. Since $$L$$ is empty, this means $$-1 \leq j < i \leq 0$$, i.e. $$j=-1$$ and $$i=0$$. We wish to show that the postcondition is true, namely, that $$L$$ is sorted and that True is returned if 0 is an element of $$L$$ and False otherwise.

Because $$L$$ is empty, it is sorted.

Because $$L$$ is empty, 0 is not an element of $$L$$, so it is vacuously true that True is returned if 0 is an element of $$L$$.

Because the loop does not execute, $$j=-1$$. Therefore False is returned. So it is indeed the case that the postcondition is true.

# If list $$L$$ is nonempty

## Entering loop

$$P(0,-1)$$ is true because $$\mathtt{range}(0,0)=\emptyset$$.

## Executing loop

Suppose that $$P(i_0,j_0)$$ is true for some $$i_0$$ and $$j_0$$ at the start of a loop execution. The loop executing means that $$i_0 < \mathtt{len}(L)$$, and combining this with $$P(i_0,j_0)$$ being true gives

1. $$-1 \leq j_0 < i_0 < \mathtt{len}(L)$$.
2. If $$x \in \mathtt{range}(0,j_0+1)$$, then $$L[x]=0$$.
3. If $$x \in \mathtt{range}(j_0+1,i_0)$$, then $$L[x]=1$$.

Either $$L[i_0]=0$$ or $$L[i_0]=1$$.

### Case $$L[i_0]=0$$

Either $$j_0+1<i_0$$ or $$j_0+1=i_0$$.

#### Subcase $$j_0+1 < i_0$$

Here, $$L[j_0+1]=1$$.

• $$j_1=j_0+1$$.
• $$L[i_0]=0$$ and $$L[j_1]=1$$ are swapped: now $$L[i_0]=1$$ and $$L[j_1]=0$$.
• $$i_1=i_0+1$$.

We want to show that $$P(i_1,j_1)$$ is true, namely

1. $$-1 \leq j_1 < i_1 \leq \mathtt{len}(L)$$.
2. If $$x \in \mathtt{range}(0,j_1+1)$$, then $$L[x]=0$$.
3. If $$x \in \mathtt{range}(j_1+1,i_1)$$, then $$L[x]=1$$.

Using $$-1 \leq j_0$$ and $$j_1=j_0+1$$, we get $$-1 \leq j_1$$.

Using $$j_0<i_0$$ we get $$j_0+1<i_0+1$$ and so $$j_1<i_1$$.

Using $$i_0< \mathtt{len}(L)$$ and $$i_1=i_0+1$$ we get $$i_1 \leq \mathtt{len}(L)$$. Hence

$-1 \leq j_1 < i_1 \leq \mathtt{len}(L)$

If $$x \in \mathtt{range}(0,j_0+1)$$, then $$L[x]=0$$. And $$L[j_1]=0$$. Hence if $$x \in \mathtt{range}(0,j_1+1)$$, then $$L[x]=0$$.

Using (3) and $$j_1 \geq j_0$$, if $$x \in \mathtt{range}(j_1+1,i_0)$$, then $$L[x]=1$$. $$L[i_0]=1$$, thus if $$x \in \mathtt{range}(j_1+1,i_1)$$, then $$L[x]=1$$.

We have established in this case that $$P(i_1,j_1)$$ is true.

#### Subcase $$j_0+1 = i_0$$

Here, $$L[j_0+1]=0$$.

• $$j_1=j_0+1$$; so $$j_1=i_0$$.
• $$L[i_0]=0$$ and $$L[j_1]=0$$ are swapped: now $$L[i_0]=0$$ and $$L[j_1]=0$$.
• $$i_1=i_0+1$$.

Using $$-1 \leq j_0$$ and $$j_0 \leq j_1$$ we get $$-1 \leq j_1$$.

Using $$j_1=i_0$$ and $$i_1=i_0+1$$, we get $$j_1 < i_1$$.

Using $$i_0< \mathtt{len}(L)$$ and $$i_1=i_0+1$$ we get $$i_1 \leq \mathtt{len}(L)$$. Hence

$-1 \leq j_1 < i_1 \leq \mathtt{len}(L)$

If $$x \in \mathtt{range}(0,j_0+1)$$, then $$L[x]=0$$. And $$L[j_1]=0$$. Hence if $$x \in \mathtt{range}(0,j_1+1)$$, then $$L[x]=0$$.

Since in this case $$j_1+1=i_1$$, here $$\mathtt{range}(j_1+1,i_1)=\emptyset$$. Thus it is vacuously true that if $$x \in \mathtt{range}(j_1+1,i_1)$$, then $$L[x]=1$$.

We have established in this case that $$P(i_1,j_1)$$ is true.

### Case $$L[i_0]=1$$

• $$j_1=j_0$$.
• $$L[i_0]=1$$ and $$L[j_1]=0$$
• $$i_1=i_0+1$$.

Using $$-1 \leq j_0$$ and $$j_1=j_0$$, we get $$-1 \leq j_1$$. Using $$j_0<i_0$$, we get $$j_1 = j_0 < i_0 < i_0+1 = i_1$$ so $$j_1<i_1$$. Using $$i_0< \mathtt{len}(L)$$ and $$i_1=i_0+1$$ we get $$i_1 \leq \mathtt{len}(L)$$. Hence

$-1 \leq j_1 < i_1 \leq \mathtt{len}(L)$

If $$x \in \mathtt{range}(0,j_0+1)$$, then $$L[x]=0$$. But $$j_1=j_0$$. Hence if $$x \in \mathtt{range}(0,j_1+1)$$, then $$L[x]=0$$.

If $$x \in \mathtt{range}(j_0+1,i_0)$$, then $$L[x]=1$$. Using $$j_1=j_0$$, if $$x \in \mathtt{range}(j_1+1,i_0)$$ then $$L[x]=1$$. And $$L[i_0]=1$$, so if $$x \in \mathtt{range}(j_1+1,i_1)$$ then $$L[x]=1$$.

We have established in this case that $$P(i_1,j_1)$$ is true.

Therefore we have shown that if $$P(i_0,j_0)$$ is true for $$i_0,j_0$$ at the beginning of the loop execution, then $$P(i_1,j_1)$$ is true for $$i_1,j_1$$ at the end of the loop execution.

## Exiting loop

Suppose that $$P(i,j)$$ is true when the loop exits. Because $$i \leq \mathtt{len}(L)$$, when the loop exits it is the case that $$i = \mathtt{len}(L)$$. Thus $$P(i,j)$$ being true means

1. $$-1 \leq j < \mathtt{len}(L)$$.
2. If $$x \in \mathtt{range}(0,j+1)$$, then $$L[x]=0$$.
3. If $$x \in \mathtt{range}(j+1,\mathtt{len}(L))$$, then $$L[x]=1$$.

It follows from this that $$L$$ is sorted in non-descending order.

$$j \geq 0$$ if and only if then there is at least one $$x$$ such that $$L[x]=0$$.

Thus when the loop exits, the postcondition is true.

This completes the proof that $$P(i,j)$$ is a correct loop invariant for the given code.