Weakest Preconditions

“Will this actually work?” THE EVERYDAY PROBLEM

Here's a tiny function. When is it safe to call? Testing a few inputs gives you some confidence. We want certainty.

def withdraw(balance):
    balance = balance - 100
    return balance

# We want one thing to always hold:
# the balance must never go negative.
#
# So AFTER running:  balance >= 0

Two Words: Before & After THE CONTRACT

Every piece of code has an implied contract: “if X is true when you call me, then Y will be true when I'm done.”

# { before:  balance >= 100 }
balance = balance - 100
# { after:   balance >= 0   }

What wp Actually Means ONE QUESTION

Why “Weakest”? = MOST PERMISSIVE

Many before-conditions would be “safe.” We want the one that rules out the fewest inputs — the most generous rule that still works.

The Whole Trick: Read It Backwards GOAL → START

Start from the goal (the “after”) and push it back through each line until you reach the start. Let's do our withdrawal, with real numbers.

# goal (after):  balance >= 0

# the line that runs:
balance = balance - 100

# Ask: for the RESULT to be >= 0,
# what must balance be BEFORE?
# The result is (balance - 100), so:
       balance - 100 >= 0
       balance >= 100   # answer!

Rule for Assignment: Copy & Replace x = e

# goal: x > 5
x = x + 1
# replace x with x+1
→ x + 1 > 5
→ x > 4

# goal: y == 10
y = y * 2
# replace y with y*2
→ y * 2 == 10
→ y == 5

# goal: total <= 50
total = total + item
→ total+item <= 50
→ total <= 50 - item

Several Lines: Go Bottom to Top ONE LINE AT A TIME

For a sequence of statements, push the goal up through the last line first, then the line above, and so on.

x = x + 1
y = x * 2
# goal (after): y > 10

Step 1 — through y = x*2
   goal y > 10, replace y with x*2
   → x*2 > 10
   → x > 5

Step 2 — through x = x+1
   need x > 5, replace x with x+1
   → x+1 > 5
   → x > 4   # final answer

if / else: Both Branches Must Work CHECK EACH PATH

For an if, the before-condition is: whichever branch runs, it must reach the goal. So check every path and require them all.

if x >= 0:
    r = x
else:
    r = -x
# goal: r == abs(x)  (r is |x|)

# when x >= 0, we run r = x
#   is x == |x|?  yes ✓ (x is non-neg)

# when x < 0, we run r = -x
#   is -x == |x|? yes ✓ (x is neg)

wp(if B: S1 else: S2, goal)
  =  (B      and wp(S1, goal))
     or
     (not B  and wp(S2, goal))

Putting It All Together ONE FULL DERIVATION

An if, then an assignment. We use all three rules, one step at a time, and never guess. All numbers are integers.

if a > b:
    m = a
else:
    m = b
m = m + 1
# goal: m > a and m > b

Step 1 — through m = m + 1 (Rule 1)
   replace m with m+1 in the goal
   → m+1 > a and m+1 > b
   → m >= a and m >= b     # integers

Step 2 — through the if (Rule 3)
   branch a > b runs m = a:
     a >= a and a >= b   → true (a > b)
   branch a <= b runs m = b:
     b >= a and b >= b   → true (a <= b)

   (a>b and true) or (a<=b and true)
   → true   # final answer

Two Traps: No else, and Code That Crashes EASY TO MISS

Python supports negative indices from -len(a). Use 0≤i only when it is part of your API's nonnegative-index convention.

if x > 10:
    x = x - 10
# goal: x <= 10

# test true : x > 10  and x-10 <= 10  → 10 < x <= 20
# test false: x <= 10 and x <= 10     → x <= 10
# together  : x <= 20

y = 10 / x
# goal: y > 2

# replace y:   10 / x > 2
# plus defined: x != 0
# solve:       0 < x < 5

Loops Are the Hard Part — Here's the Idea DON'T UNROLL

Invariants yield sufficient conditions; the exact total-correctness weakest precondition has a least-fixed-point characterization and is not computable for arbitrary programs.

An arbitrary loop needs a fixed-point or inductive argument rather than one assignment-style substitution. Invariants plus a well-founded variant prove sufficient input conditions; they need not produce the exact weakest precondition.

Finding the Invariant — a Real Loop SUM 1..n

Add up 1 + 2 + … + n. Watch what stays true after every pass — that's the invariant.

i = 0
s = 0
while i != n:
    i = i + 1
    s = s + i
# goal: s == 1+2+...+n

Proving It Stops — the Bound A COUNTDOWN

The Loop Checklist (All Together) 4 QUICK CHECKS

Once you have an invariant P and a bound t, a correct loop is just these four checks. Here they are for the sum loop.

Loop Example 2: Linear Search FIND THE FIRST x

Look through list b (length n) for the first place that holds x. Same four checks, new loop.

i = 0
while i < n and b[i] != x:
    i = i + 1
# goal: i == n  and x is not in b
#   or  i < n   and b[i] is the FIRST x

Loop Example 3: Binary Search HALVE EACH PASS

The list a is sorted. Find the leftmost spot where x could go. This loop is famous for off-by-one bugs; the invariant removes them.

lo, hi = 0, len(a)
while lo < hi:
    mid = (lo + hi) // 2
    if a[mid] < x:
        lo = mid + 1
    else:
        hi = mid
# goal: everything in a[:lo] < x
#       everything in a[lo:] >= x

 0          lo           hi          n
 |  all < x  |  not seen  |  all >= x |

Three Sanity Facts About wp QUICK INTUITION

You don't need these to use the method, but they explain why it behaves so predictably.

You Already Half-Do This EVERYDAY PAYOFF

You don't have to write formal proofs to benefit. The habits show up directly in code you write today.

def withdraw(balance, amt):
    assert balance >= amt   # the wp!
    return balance - amt
# the assert IS the weakest
# precondition, written down.

Common Mistakes (and the Quick Fix) STUDENT TRAPS

Almost every wrong answer on a wp exercise is one of these six.

Check Yourself TRY FIRST, THEN OPEN

Work each one on paper. Then click “Answer” to compare. All variables are integers.

i, p = 0, 1
while i != n:
    p = p * 2; i = i + 1
# goal: p == 2**n

i = 0
while i < n:
    if b[i] == 0: continue
    i = i + 1

Glossary EVERY WORD IN ONE PLACE

The Cheat Sheet ONE PAGE