An Axiomatic Basis for Computer Programming

At the loop header use a = bq + r and r ≥ 0. Between the two assignments the same header invariant need not yet hold; derive the assertion that connects them.

At initialization, q=0 and r=a, so a=bq+r and r≥0. Suppose the invariant and guard r≥b hold. After r := r-b, the intermediate assertion is a=bq+r+b, with the new r nonnegative. After q := q+1, that assertion becomes a=bq+r again because the new q absorbs the extra b. This explicitly respects sequential assignment rather than pretending both variables changed simultaneously.

At termination the false guard gives r<b, so together with the invariant we have a=bq+r and 0≤r<b. These characterize quotient and remainder for positive b. For termination, r is a nonnegative integer at each header and decreases by the positive amount b on every iteration. It cannot decrease indefinitely while remaining nonnegative.

For (17,5), header states (q,r) are (0,17), (1,12), (2,7), and (3,2). On the first subtraction, the transient state is (0,12), satisfying 17=5×0+12+5; the following increment restores the header equation. The answer is quotient 3 and remainder 2.

If b=0, the guard remains true, r never decreases, and q increases forever. The equation a=bq+r remains true throughout, so invariant preservation alone does not establish termination. Hoare explicitly distinguishes conditional correctness from successful termination. The proof also assumes mathematical integers and side-effect-free expressions; a bounded implementation must justify overflow behavior and resource limits separately.

Check your reasoning

• Proves initialization, the intermediate assertion, preservation, and the exit condition.
• Uses r as a decreasing natural-number variant under b>0.
• Shows b=0 can preserve the invariant while failing to terminate.

Negating the minimum signed value produces a bit pattern that still represents the minimum signed value. Define the wrap function explicitly before testing.

Over mathematical integers the weakest precondition is true: nonnegative inputs are left unchanged, and negating a negative integer gives a positive integer. In the eight-bit wrapping model, every input except -128 satisfies the postcondition. Negating -128 gives mathematical 128, whose wrapped signed interpretation is -128 again. Thus the weakest precondition is x ≠ -128 within the declared input domain.

def wrap8(n):
    return (n + 128) % 256 - 128
def abs8(x):
    return wrap8(-x) if x < 0 else x
failures = [x for x in range(-128,128) if abs8(x) < 0]
assert failures == [-128]
assert all(abs8(x) == abs(x)
           for x in range(-127,128))

For the stronger specification, all allowed inputs except -128 again succeed. The mathematical absolute value of -128 is 128, which cannot be represented in the output type. Satisfying that specification for every input requires widening the output representation or changing the interface to report an exceptional case. A different language may trap or have undefined signed-overflow behavior rather than wrap, so this model cannot be silently applied to it.

The finite enumeration verifies every input in this particular machine domain, while the reasoning identifies why the exceptional value exists. Hoare's axiomatic method requires the implementation to satisfy the arithmetic axioms used by the proof. Identical-looking source text can denote different state transformations under different numeric semantics; a proof of one transformation does not automatically prove another.

Check your reasoning

• Derives true over integers and x≠-128 over signed wrapping eight-bit values.
• Enumerates exactly one failing input and explains representation limits.
• Distinguishes wrapping, trapping, and other language semantics.