Proving correctness of search algorithms

Question

I've seen correctness proofs for other searching algorithms; however, for this particular algorithm: search in a row-wise and column wise sorted matrix, I'm not able to generate a proper proof.

The algorithm is

Let x = element we're trying to search for in the matrix,
 e = current element we're processing in the array.
1) Start with the top right element.
2) Loop: compare this element e with x
...i) if e = x, then return the position of e, since we found x in the given matrix.
...ii) if e > x then move left to check elements smaller than e (if out of binding of the matrix, then break and return false)
...iii) if e < x then move below to check elements greater than e (if out of binding of the matrix, then break and return false)
3) repeat the i), ii) and iii) until you find the element or return false

Essentially, we start from the top right and traverse to the bottom left, key points being if element we're searching for is smaller then we go left if it's bigger we traverse down.

I'd like to use contradiction by saying the following: "If we traversed all the way to the bottom left of the algorithm and we didn't find the element we're searching (assuming it's in the matrix), then ..."

However, I'm not sure how to properly follow up the "then" because whatever I say is just repeating what the algorithm does, not really proving anything.

Is there a proper way to do this? Perhaps induction? (but this seems ever more complicated)

• Raphael: The correct lemmas aka invariants are usually the way to go.

Answer 1

The idea of the algorithm is to maintain the following invariant:

If $x$ is in the matrix, then it is in the submatrix whose top right corner is $e$.

The invariant clearly holds in the beginning, since $e$ is the top right corner of the original matrix.

If $e > x$ then all elements below $e$ are also larger than $x$, and so $x$ cannot be contained in that column. Therefore the invariant continues to hold with $e$ replaced with its left neighbor (if $e$ has no left neightbor, we can deduce that $x$ is not found in the matrix).

If $e < x$ then all elements to the left of $e$ are also smaller than $x$, and so $x$ cannot be contained in that row. Therefore the invariant continues to hold with $e$ replaced with its neighbor below (if any).

On an $n \times m$ matrix, this process terminates in at most $n+m$ steps, either finding $x$ or determining that it does not appear in the matrix.

• user40759: Wow, I never thought of using loop invariant in such a manner, thank you for the insight.
• xuq01: @Jonathan Invariants are powerful tools in verification of imperative programs! Check out Hoare logic too.