Binary Search Contract Lab
정답 코드를 외우는 화면이 아닙니다. specification을 고르고, 결과와 반례를 예측하고, comparison/update/return만 bounded patch한 뒤, 작은 입력을 전수 검사합니다. 각 source semantic step을 후보 영역·불변식·종료 measure와 함께 replay하고 다른 monotone predicate로 옮깁니다.
같은 코드를 universal label로 평가하지 않는다
function boundarySearch(a, target) {
let lo = 0;
let hi = a.length;
while (lo < hi) {
const mid = lo + Math.floor((hi - lo) / 2);
if (a[mid] < target) {
lo = mid;
} else {
hi = mid;
}
}
return lo;
}It returns the lower_bound only on paths that never need to discard mid from the left; it is not a total lower_bound implementation.
a = [1], target = 2: lo = 0, hi = 1, mid = 0, then lo = mid leaves the measure 1 -> 1.
The answer boundary may remain inside [lo, hi], so partial correctness alone does not prove termination.
Not established. The true branch can preserve hi - lo, and the lab stops with non-termination evidence immediately.
No finite comparison bound on the counterexample; auxiliary algorithm state is O(1).
No new reuse is created by retaining mid; the update contradicts the half-open progress contract.
Non-shrinking half-open update · deterministic counterexample replay
array is sorted ascending
Inclusive [lo, hi]
- initial
- lo = 0, hi = n - 1
- guard
- lo <= hi
- discard
- lo = mid + 1 / hi = mid - 1
- empty
- lo > hi
- measure
- hi - lo + 1
Half-open [lo, hi)
- initial
- lo = 0, hi = n
- guard
- lo < hi
- discard
- lo = mid + 1 / hi = mid
- empty
- lo === hi
- measure
- hi - lo
작은 배열 테스트가 숨기는 integer midpoint overflow
EXACT operands: lo=1,500,000,000, hi=2,000,000,000. Java의 signed 32-bit addition을 별도로 모델링했습니다. 이 숫자는 배열을 실제 할당하거나 wall-time을 측정한 결과가 아닙니다.
Specification을 먼저 잠근다
a is sorted ascending; duplicates are allowed.
Return the smallest i in [0, n] such that i === n or a[i] >= target.
A linear scan stops at the first value that is not below target; n is the sentinel result.
P(i) := a[i] >= target.
결과와 failure mode를 보기 전에 예측한다
comparison / update / return만 bounded patch한다
이 editor는 JavaScript executor가 아닙니다. 전체 13줄 skeleton을 검사한 뒤 네 finite semantic token만 pure interpreter에 전달합니다. source는 browser 밖으로 보내거나 compile하지 않습니다.
prediction receipt를 잠그면 patch editor가 열립니다.
작은 입력 전수 검사로 최소 반례를 찾는다
예측 receipt를 먼저 잠가야 합니다.