Beginner Question Concerning the Logic of a Very Simple Correctness Proof

Question

I'm trying to familiarize myself with correctness proofs and need some help. In the proof for SimpleSelect (P.25), why do we assume both $A'[i] < A'[k]$ and $1 \leq i \leq k$? I'm not quite sure why we do this, as the text states that because "of what it means for an algorithm to meet its specification, any proof of correctness will begin by assuming the precondition." However, isn't the precondition here simply the precondition of SimpleSelect as specified here (P.6)?

Answer 1

Both of the assumptions you mention are "local" in the sense that they are a subclaim in the proof and are not part of the conditions of the theorem. You can also see them as the definition of a local variable $i$, an equivalent formulation of the two assumptions would be

1. Let $i$ be such that $A'[i]<A'[k]$ and $1\leq i \leq n$.

2. Let $i$ be such that $1\leq i \leq k$.

The proof counts the number of values of $i$ for which these statements hold, which shows that the postcondition is satisfied.

---

I think part of your confusion follows from some implicit language in these paragraphs, so I will rewrite one of them in full to be more explicit. The first paragraph from the book reads:

Suppose $A'[i] < A'[k]$ for some $i$, $1 \leq i \leq n$. Then $i < k$, for if $k < i$, $A'[k] > A'[i]$ violates the postcondition of Sort. Hence, there are fewer than $k$ elements of $A'$ , and hence of $A$, with value less than $A' [k]$.

A more explicit phrasing is as follows:

Let $i$ be such that $A'[i]<A'[k]$ and $1\leq i \leq n$. If $k<i$, then $A'[i]<A'[k]$ contradicts with the postcondition of Sort, so $i\leq k$. If $i=k$, then $A'[i]=A'[k]$, which contradicts with our definition of $i$.

So, we have shown that if $A'[i]<A'[k]$ and $1\leq i \leq n$, then $i<k$. This means that the number of elements of $A'$ with value strictly less than $A'[k]$ is strictly fewer than $k$. Since $A$ is a permutation of $A'$, there are fewer than $k$ elements of $A$ strictly less than $A'[k]$. Since $A'[k]$ is the return value of the algorithm, the first part of the postcondition of Select is satisfied.

The overall structure of the second paragraph is similar, so you should be able to grasp it if you can understand the first.