Loops and Program Correctness
A precondition is a condition that must be true before a piece of code runs, and it is used to ensure a program is correct.
Why a Program That Runs Can Still Be Wrong
A program can run without errors and still produce the wrong answer, or no answer at all, when it receives input its author never considered. Many beginners assume that once a program compiles and prints something plausible, its logic must be right. This article examines that assumption using a small program segment that solves a quadratic equation. The segment is short, but it shows a disciplined way of reasoning about why each line can be trusted.
The misconception this article targets is the belief that a program will always produce an exact, trustworthy result simply because its formula looks right. A quadratic formula is mathematically sound, but a line of code that applies it is only correct when the values fed into it satisfy the conditions the formula depends on.
What do you think happens?
Before reading the source program, what do you think its loop guarantees about the values A, B, and C before the root is computed?
Reveal answer
That A is nonzero and the discriminant is nonnegative.
The check does not happen where the formula is written. It happens earlier, in a loop that keeps asking for input until the input is acceptable. The loop establishes the conditions the formula needs before the formula runs.
Preconditions: What Code Requires
A precondition is a condition that must be true before a piece of code runs, and it is used to ensure a program is correct.
In the quadratic solver, the lines that compute the discriminant and the root depend on two requirements. The first is that the coefficient A must not be zero, because the formula divides by 2 times A. The second is that the discriminant, B squared minus 4 times A times C, must be greater than or equal to zero, because the formula takes a square root of it, and the source treats a negative discriminant as having no real solution. Together these two requirements form the precondition for the final two lines of the segment.
- 1A must be nonzero because the root formula divides by 2A
- 2The discriminant D = B2 - 4AC must be nonnegative because the root formula takes the square root of D
- 3Both conditions must hold at the same moment, just before the last two lines run
Postconditions: What Code Guarantees
A postcondition is a condition guaranteed to be true after a piece of code runs, and it is valid only when the preconditions before it hold.
In the quadratic solver, the postcondition of the last two lines is that x is a solution of the equation A times x squared plus B times x plus C equals zero. The source points out that this postcondition is valid because the preconditions for those two lines are fulfilled when the loop ends. The logical chain has a clear order: the precondition is established first, and the postcondition follows from it.
Tracing a Validation Loop Step by Step
The source program segment has two stages. The first stage is a do-while loop that prints instructions, reads values for A, B, and C, and then checks the preconditions. If the check fails, it prints a message and repeats. The second stage computes the discriminant and the root, and it runs only after the loop has exited. Because the loop exits only when the check passes, the second stage never begins with invalid inputs.
To see how the state changes, trace a run with three attempts. These input values are an illustrative example written for this article, not taken from the source. Watch which condition each attempt satisfies and which one first makes the loop exit.
Checking the Final Attempt Against the Postcondition
After the third attempt passes, compute the root and confirm that it satisfies the postcondition for A = 1, B = -3, C = 2.
- 1Check the preconditions
A = 1 is not zero. The discriminant is B2 - 4AC = 9 - 8 = 1, which is greater than or equal to 0. Both preconditions hold, so the root lines may run.
- 2Compute the roots
The root formula gives x = (3 plus or minus the square root of 1) divided by 2, so x = 2 or x = 1.
- 3Verify the postcondition
For x = 2, A x2 + B x + C = 4 - 6 + 2 = 0. For x = 1, the value is 1 - 3 + 2 = 0. Both roots satisfy the postcondition.
The postcondition holds because the loop established the preconditions before the root lines ran.
Locating Where the Promise Breaks
A divergence happens when the code after a point assumes a precondition that no longer holds. In the trace above, the first attempt, with A equal to zero, is the point where a naive program would fail: the root formula divides by 2A, so the stated precondition for the root lines is violated. The attempt with C equal to 5 shows a second kind of violation: the discriminant is negative, so the square root has no real value under the source's treatment. In both cases the check is what stops the divergence from reaching the root computation.
To locate a divergence, ask three questions at each line. What must be true on entry? What does this line assume? Does the state at this point actually satisfy that assumption? The first point where the answer to the last question is no is where the expected result stops matching the promise.
Two Ways to Enforce a Precondition
The source presents a loop-based check, in which the program keeps asking for input until the preconditions hold. It also presents a second variation in which the precondition is checked by an if statement. Inside the if branch, the program knows that the preconditions hold, so it can compute and print the solution. In the remaining branches, the program knows that one of the preconditions fails, and it reports why.
In either variation, the program is correct for the same reason. Every path either satisfies the preconditions before the computation or reports that they fail. The root computation is therefore never reached in an unsafe state.
Mistakes That Break the Guarantee
Common mistake Assuming a correct formula guarantees a correct result
What it looks likeA program applies the quadratic formula directly to whatever A, B, and C the user typed.
Why it failsThe formula is only valid when its preconditions hold. A zero A or a negative discriminant breaks the conditions the formula depends on.
Do this insteadState the preconditions and enforce them before the formula is applied.
Common mistake Writing a validation check that does not cover every precondition
What it looks likeA loop checks only that A is not zero and never checks that the discriminant is nonnegative.
Why it failsThe root computation still receives inputs that violate one of its preconditions, so its postcondition is no longer guaranteed.
Do this insteadWrite one check that tests all the preconditions the following code needs.
Common mistake Placing the check after the computation that needs it
Why it failsA check that runs after the computation cannot protect that computation, because the unsafe step has already happened.
Do this insteadPlace the check before the first line that depends on the precondition.
Common mistake Trusting a postcondition without tracing its preconditions
Checking Exact Values on a Machine
The source notes that real-number representation on computers means an algorithm can be correct on paper while its program is not a perfect implementation. A precondition is a reasoning tool that makes a program easier to trust, but it does not remove every source of error.
When you write a precondition, ask whether the check you write can be evaluated exactly by the machine. If it cannot, consider how close the stored value is to the mathematical value you intended.
Finding the Divergence in a Partial Check
Suppose the validation loop for the quadratic solver checks only that A is not zero and omits the discriminant check. The user enters A = 1, B = 2, C = 5. Which precondition of the root computation fails, at which line would the program take a square root of a negative number, and what does the postcondition promise that the program can no longer deliver?
Hints
- Compute the discriminant B2 - 4AC for these values before deciding anything.
- The root lines are only safe when every precondition holds at the moment they run.
- Compare what the postcondition says x must satisfy with what a computed value would actually be.
Key Takeaways
- A precondition is a condition that must be true before a piece of code runs. In the quadratic solver, the preconditions are that A is not zero and the discriminant B squared minus 4AC is greater than or equal to zero.
- A postcondition is a condition guaranteed after a piece of code runs, and it is valid only when the preconditions before it hold.
- A validation loop or if check establishes the preconditions, which makes the code that follows it safe to run.
- A divergence appears at the first point where the state no longer satisfies a precondition that the following code assumes. Tracing state line by line locates that point.
- Preconditions are reasoning tools, not guarantees against every error. Real-number representation on computers can still separate a correct algorithm from a perfect implementation.