Combine initialization, maintenance, exit reasoning and a decreasing measure.
Loading your saved responses…
Try
A loop can give the right answer in several tests and still fail at an untested boundary. A correctness proof states what stays true at each loop boundary, then explains how that fact yields the desired result when the loop stops.
Predict
Predict the two separate obligations: partial correctness says a terminating execution has the right result; termination says execution actually stops. An invariant must hold initially and be preserved. A decreasing nonnegative integer measure often proves termination.
Experiment
Trace lower-bound search on sorted values [1,3,3,7] with target 3. Start lo=0,hi=4. At each midpoint, record which indices are known below the target and which are known to qualify. Keep the upper endpoint exclusive; the final answer should be index 1, not an arbitrary matching index.
Lower-bound search for target 3 in sorted [1,3,3,7] returns index 1. The second 3 at index 2 is a match but not the first qualifying index; the task is more specific than finding any match.
Understand
Worked binary-search invariant: indices below lo have values below t, and indices at or above hi have values at least t. If a[mid]<t, sortedness allows lo=mid+1. Otherwise hi=mid. Both updates preserve the assertions, and width hi−lo strictly decreases whenever positive. At exit lo=hi is the first qualifying index, with the array length representing no qualifying value.
A summation loop has a different invariant: before iteration i, s is the sum through i−1. Adding i establishes the next case; the exit index converts the invariant to the postcondition.
Invalid termination argument: the interval never grows, so it must end. Keeping lo=mid when width is one can leave the same interval forever; strict decrease is needed.
Apply
State loop boundaries precisely and include empty-input behavior. Test the invariant after each branch, not just after a typical branch. To prove termination, explain why the measure is bounded below and decreases by at least one in the integer setting.
Continue
Depth: total correctness combines invariant reasoning and termination. More complex algorithms use lexicographic measures or well-founded orders. Machine implementations additionally need bounds, overflow and representation checks that an ideal integer proof may omit.
Apply · explain · revise
Practice and reasoning
Drafts save locally as you type. Reveal worked solutions when useful; the site remembers that exposure. Automatic matches check the requested answer, while written arguments require review against the rubric.
A loop starts s=0 and adds integers 1 through 8. What is its final s?
Integers, fractions and finite decimals are accepted. Expressions such as sqrt(2) are not parsed by this checker.
A lower-bound binary search on [lo,hi) starts [0,8). With every comparison taking the branch hi=floor((lo+hi)/2), how many comparisons until lo=hi?
Integers, fractions and finite decimals are accepted. Expressions such as sqrt(2) are not parsed by this checker.
A loop invariant must hold:
A standard termination proof uses a quantity that:
Prove the loop 's=0; for i=1,...,n add i to s' computes n(n+1)/2 for every n≥0.
Structure your argument and preserve revisions
These optional planning fields save locally. Recording your response saves an immutable copy of the argument and these fields. Older records may contain only first/latest responses; missing intermediate revisions are not reconstructed.
Each field allows 2,000 characters. Keep a specific claim, state where it applies, cite the facts you use, and explain what still needs checking. Blank fields are allowed and are not evidence of mastery.
For sorted array a and target t, lower-bound search maintains [lo,hi), with all indices below lo having a[i]<t and all indices at or above hi having a[i]≥t. Explain updates and termination.
Structure your argument and preserve revisions
These optional planning fields save locally. Recording your response saves an immutable copy of the argument and these fields. Older records may contain only first/latest responses; missing intermediate revisions are not reconstructed.
Each field allows 2,000 characters. Keep a specific claim, state where it applies, cite the facts you use, and explain what still needs checking. Blank fields are allowed and are not evidence of mastery.
Reflect and continue
Before marking this lesson complete, explain one key idea without the worked solution and identify a condition that matters. Marking complete records participation, not independent mastery.
