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))

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

You can't “substitute backward” through a loop — it might run 3 times or 3 million. Instead we describe the loop with two things we invent, then check a short list.

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.

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.

The Cheat Sheet ONE PAGE