3
$\begingroup$

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)?

$\endgroup$
2
$\begingroup$

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.

$\endgroup$
6
  • $\begingroup$ So the 2 assumptions you stated are two different cases for which the postcondition of Sort would be true? If yes I still don't see how the postcondition translates into sub-assumptions 1 and 2. The postcondition of Sort is: "A[1..n] is a permutation of its initial values such that for 1 ≤ i < j ≤ n, A[i] ≤ A[j]." $\endgroup$ May 17 '20 at 17:21
  • $\begingroup$ @MoritzWolff No, the two assumptions are used to prove the postcondition of SimpleSelect. The two paragraphs with these 2 assumptions each prove a part of the postcondition of SimpleSelect, using the postcondition of Sort. $\endgroup$
    – Discrete lizard
    May 17 '20 at 17:43
  • $\begingroup$ Thanks for your answer, but I still have some doubts. So are the two assumptions arbitrary? But then we would only proove that IF the given assumption is true THEN the respective parts of the postcondition of SimpleSelect are true. Which is not what we are searching for. We want the parts of the postcondition to follow from the previous statements without a dependency on an arbitrary assumption. $\endgroup$ May 18 '20 at 9:03
  • $\begingroup$ @MoritzWolff No, what you describe is not how the proof is structured. The first part is a proof that an implication $A \Rightarrow B$ holds. The second part uses the implication to derive that the postcondition is true. This proof is independent of whether $A$ is true or not. I edited my answer to make the paragraph more explicit. If you still have doubts after reading it, please point to a specific part of my write-up here you do not follow. $\endgroup$
    – Discrete lizard
    May 18 '20 at 11:13
  • $\begingroup$ The structure of the proof makes sense now. How would I translate the first part of the subcondition of SimpleSelect into a more formal language? "there are fewer than k elements A[i] < x" intuitively seems to be equivalent to "For all i, if A[i] < x, then the biggest possible value for i is k." But it doesn't really work out like this. I would like to see how the proposition that is the first part of the subcondition is logically structured. $\endgroup$ May 18 '20 at 18:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.