Skip to main content

Correctness and Termination Practice

Allow 60–90 minutes. Use the worked examples only for the first attempt, then close them. Solutions are separate.

  1. B1: Prove lower_bound on sorted integers using a half-open invariant and variant. Trace [2,2],target 2. Why is returning immediately on equality wrong?
  2. B2: A binary search sets lo=mid when a[mid]<target. Find a smallest nonterminating input and repair the update. State the decreasing measure.
  3. B3: Prove recursive array maximum correct for nonempty arrays, splitting into two nonempty halves until singletons. State induction hypothesis, combine lemma, termination measure, and the empty-input contract.
  4. B4: A nested process can move from pair(3,2) to(2,100). Does this decrease a lexicographic natural-number rank? Explain the precise ordering and why bounded-below real values that merely decrease do not establish termination.
  5. B5: Subset-sum search prunes when current_sum exceeds target. Refute this for signed values, then state a domain where the pruning is sound and justify it.

For a repair, preserve the first failed invariant or counterexample and redo one changed case. Testing a proof's example does not replace its quantified argument.