Imperative Programming Part 1.
A loop invariant is a property of the program state that holds whenever control reaches the loop's condition, including the final failed test. Its main purpose is proving partial correctness: establish it initially, prove one guarded iteration preserves it, then combine it with the negated condition to obtain the postcondition. A separate loop variant or another progress argument proves algorithm termination and hence total correctness.
The proposed condition is not a loop invariant at the loop head. It holds initially and on entry to every executed body, but the iteration starting with
i == 10 finishes with i == 11. Control then returns to the condition with the proposed upper bound false. A suitable numerical loop invariant is . If the number of printed lines matters, strengthen it to “exactly lines have been printed.” At exit, this and i > 10 give exactly ten printed lines. The nonnegative loop variant decreases by one on every iteration.This is lower-bound search: return the first position whose value is at least the target, allowing the result to equal the array length. The notation for an empty suffix is vacuously true, so this also covers a target larger than every entry and the empty array. Assume a stable sorted array, ordered nondecreasingly.
def ternarySearch(a: Array[Int], x: Int): Int = {
var lo = 0
var hi = a.length
while (lo < hi) {
val third = (hi - lo) / 3
val m1 = lo + third
val m2 = hi - 1 - third
if (a(m1) >= x) hi = m1
else if (a(m2) < x) lo = m2 + 1
else {
lo = m1 + 1
hi = m2
}
}
lo
}The loop invariant isInitially the excluded prefix and suffix are empty, so both quantified assertions hold. During an iteration, . If , sortedness makes every later value at least , so replacing
hi by m1 preserves the right assertion. If the first test failed and , every earlier value is below , so replacing lo by m2 + 1 preserves the left assertion. Otherwise ; both new exclusions are valid, and lo = m1 + 1; hi = m2 retains exactly the unresolved middle. In that branch , since a single value cannot satisfy both strict and nonstrict inequalities in opposite directions.The nonnegative loop variant
hi - lo strictly decreases. In fact, with old length and , the three possible new lengths are , with the middle branch feasible only when nonnegative; each is at most . At exit lo == hi, and the loop invariant is exactly the desired partition. The result is the unique lower-bound index, including the first equal entry when duplicates occur. This ternary lower-bound search uses comparisons and auxiliary space, in the Big O notation word-operation model. The index formulas also avoid computing an overflowing 2 * length.For the given sorted array, the complete lower-bound search behavior is for , for , for , and for . In particular, index is never the correct answer because the two equal entries share the same first insertion position.
These unit tests cover every value boundary, equality case and missing-value interval:
- Below all entries, including the smallest machine integer:
ternarySearch(a, Int.MinValue) == 0andternarySearch(a, 0) == 0. - Equality with the first entry:
ternarySearch(a, 1) == 0. - Values in the first gap:
ternarySearch(a, 2) == 1andternarySearch(a, 3) == 1. - Repeated equality must return the first duplicate:
ternarySearch(a, 4) == 1. - Values in the second gap:
ternarySearch(a, 5) == 3andternarySearch(a, 9) == 3. - Equality with the final entry:
ternarySearch(a, 10) == 3. - Beyond the final entry:
ternarySearch(a, 11) == 4andternarySearch(a, Int.MaxValue) == 4.
For every tested target, also assert that the array is unchanged, the result lies in , every entry before it is strictly smaller, and every entry from it onward is at least the target. These postconditions check the intended partition directly rather than merely accepting any equal occurrence.
Search only the suffix strictly after each candidate first index. This enforces distinct indices even when the target is twice an existing value. Compute the complement in
Long to prevent integer overflow: subtracting two Int values can require 33 signed bits.def twoSum(a: Array[Int], target: Int): (Int, Int) = {
def lowerBound(from: Int, wanted: Long): Int = {
var lo = from
var hi = a.length
while (lo < hi) {
val mid = lo + (hi - lo) / 2
if (a(mid).toLong < wanted) lo = mid + 1
else hi = mid
}
lo
}
var i = 0
while (i < a.length - 1) {
val wanted = target.toLong - a(i).toLong
val j = lowerBound(i + 1, wanted)
if (j < a.length && a(j).toLong == wanted) return (i, j)
i += 1
}
(0, 0)
}The outer loop invariant says that no solution has a smaller first index than
i, when a pair is written in increasing index order. A failed suffix binary search proves there is no partner for the current i, extending the excluded prefix by one. A successful return has and in exact integer arithmetic. At exhaustion, every possible ordered pair has been excluded, so the sentinel (0,0) means no solution. The inner loop invariant is the standard lower-bound partition, restricted to the suffix starting at i + 1.There are at most suffix searches, each taking running time, so the total is , customarily written for . Auxiliary space is . Empty and singleton arrays immediately return the sentinel. This is distinct-index two-sum by suffix lower bounds; a faster two-pointer technique is also possible on a sorted array, but the code here directly meets the requested search-based bound.
Articles by others on the same topic
There are currently no matching articles.