Skip to main content

Model Artifact: Proof Notebook

Scenario​

A learner is proving correctness for binary search before implementing the iterative version in Semester 1/2 transition work.

Completed learner-quality example​

Claim​

For a sorted array A[0..n-1] and target x, iterative binary search returns an index i with A[i] = x when one exists, and returns not_found otherwise.

Definitions and preconditions​

  • A is sorted in nondecreasing order.
  • The active search interval is the inclusive range [lo, hi].
  • Values outside [lo, hi] have already been ruled out.

Loop invariant​

At the start of every loop iteration, if x occurs in A, then at least one occurrence of x lies inside A[lo..hi].

Initialization​

Before the first iteration, lo = 0 and hi = n - 1, so the active interval is the full array. If x occurs anywhere in A, it lies inside this interval.

Maintenance​

Let mid = lo + floor((hi - lo) / 2).

  • If A[mid] = x, the algorithm returns a correct witness immediately.
  • If A[mid] < x, sortedness implies every index j <= mid has A[j] <= A[mid] < x; those positions cannot contain x, so setting lo = mid + 1 preserves the invariant.
  • If A[mid] > x, sortedness implies every index j >= mid has A[j] >= A[mid] > x; those positions cannot contain x, so setting hi = mid - 1 preserves the invariant.

Termination​

Each non-returning iteration strictly shrinks the interval length hi - lo + 1. The loop terminates when lo > hi, meaning the active interval is empty. By the invariant, if x occurred in A, it would have to be in the empty interval, which is impossible. Returning not_found is therefore correct.

Edge cases checked​

  • Empty array: initial hi = -1, loop does not run, not_found is correct.
  • Single element: either the midpoint matches or the interval becomes empty after one comparison.
  • Duplicates: the claim requires any matching index, not the first matching index.

How to read this example​

  • Passing: States a precise claim, names preconditions, and uses initialization/maintenance/termination rather than intuition.
  • Strong: Connects every interval update to sortedness and explicitly handles the empty-interval conclusion.
  • Portfolio-worthy: Includes edge-case analysis and a claim scoped carefully enough to avoid overclaiming first-occurrence behavior.