CS292C-4: Computer-Aided Reasoning for Software
Lecture 4: Hoare Logic II + Verification Condition Generation (VCG)
Spring 2025 | Prof. Yu Feng

by Yu Feng

Why Loops Are Hard
Run Forever
Loops may not terminate
State Dependent
Behavior changes with program state
Require Insight
Need deeper understanding to verify
We need loop invariants
Loop Rule (Hoare Logic)
The standard inference rule format:
{ I ∧ b } C { I }
──────────────────
{ I } while b do C { I ∧ ¬b }
where I is the loop invariant
This rule states that if the invariant I combined with the loop condition b is preserved by each execution of the loop body C, then executing the entire while loop starting with I will result in I and the negation of b.
What's a Loop Invariant?
Initial Condition
Holds before loop starts
Preservation
Preserved after each iteration
Usefulness (Inductive)
Helps prove postcondition
You supply I manually
Intuition: Multiplying by Addition
Code
// Goal: y = 3 * x
i := 0; y := 0;
while i < x do {
  y := y + 3;
  i := i + 1;
}
Invariant
y = 3 * i ∧ i ≤ x
Captures relationship between variables at each step
Proof Sketch
Initialization
i = 0, y = 0 ⇒ I holds
Preservation
I ∧ i < x ⇒ I after iteration
Postcondition
I ∧ ¬(i < x) ⇒ i = x ⇒ y = 3 * x ✓
Loop rule proves partial correctness
Loop Invariant Construction Tips
Think About Change
What changes, what stays true
Specific Techniques:
Shadow Variables
Track original values
Loop Unrolling
See patterns in iterations
Logical Bounds
Add constraints (e.g., x ≤ n)
Common Loop Invariants
Counters
i ≤ n
Accumulators
sum = ∑
Index Relations
arr[i] ≤ key
Numeric Relationships
y = 3 * i
Practice helps
Houdini: Automatic Loop Invariant Inference
Houdini is an algorithm created by Microsoft Research that automatically finds loop invariants - one of the hardest parts of proving programs correct.
Candidate-Based Approach
Houdini begins with many possible invariants and removes those that don't work when the program runs.
Conjunctive Invariants
Works with simple statements joined by "and" (like x ≥ 0 and y = x+1), making it fast but limited.
Fixed-Point Computation
Uses a special method to find the strongest valid invariant from all the candidates.
While Houdini was a big step forward in finding invariants automatically, finding complex loop invariants by computer is still an unsolved problem. Today's methods use machine learning and other techniques, but still often need human help.
Citation: Flanagan, C. and Leino, K.R.M. "Houdini, an Annotation Assistant for ESC/Java", FME 2001: Formal Methods for Increasing Software Productivity.
Exercise: Try It
Code
i := 0;
sum := 0;
while i < 5 do {
  sum := sum + i;
  i := i + 1;
}
Question
What is a good invariant?
Hint: sum = 0 + 1 + ... + (i - 1)
Correct loop invariant: sum = Σ(j=0 to i-1) j
Or equivalently: sum = (i * (i - 1)) / 2
Annotating a Loop
1
Precondition
{ true }
2
Initialization
i := 0; sum := 0; { sum = 0 ∧ i = 0 }
3
Loop with Invariant
while i < 5 { { sum = 0 + ... + (i-1) }
4
Loop Body
sum := sum + i; i := i + 1; }
5
Postcondition
{ sum = 0 + ... + 4 = 10 }
Motivation for VCG
Manual Proofs
Slow and error-prone
Key Question
Can we generate proof obligations mechanically?
Answer
Yes, with Verification Condition Generation
What is a VC?
Definition
A verification condition (VC) is a logical formula
Validity
If VC is valid, program is correct
Source
Generated from Hoare rules
Weakest Precondition (WP)
Definition
wp(C, Q) = weakest condition P such that {P} C {Q}
Direction
Backward analysis
Start from postcondition, walk backward to find pre
WP Examples
Example 1
C: x := x + 1
Q: x = 2
wp(C, Q) = x + 1 = 2 ⇒ x = 1
Example 2
C: x := y + 2
Q: x ≥ 0
wp = y + 2 ≥ 0 ⇒ y ≥ -2
VC Generation Pipeline
Annotate
Add invariants to code
Compute WP
Work backward from postcondition
Emit Conditions
Generate logical formulas
Solve
Feed into SMT solver (e.g., Z3)
VCs ≈ automated Hoare logic proofs
Example: VC for Assignment
General Rule
For an assignment statement x := E and postcondition Q:
wp(x := E, Q) = Q[x/E]
where Q[x/E] means "substitute all occurrences of x in Q with E"
Example
Consider this assignment and postcondition:
x := x + 1
{x = 2}
Computing the VC
The verification condition is generated as follows:
wp(x := x + 1, x = 2) 
  = (x = 2)[x/x+1]    // Substitute x+1 for x
  = (x+1 = 2)         // Apply substitution
  = (x = 1)           // Simplify
VC for Skip
Definition
The skip statement does nothing and immediately terminates.
General Rule
For a skip statement and postcondition Q: wp(skip, Q) = Q
Skip doesn't change any program state, so weakest precondition equals postcondition.
Example
For skip {x = 5}, the VC is: wp(skip, x = 5) = (x = 5)
To ensure x = 5 after skip, x must equal 5 before skip.
VC for Sequence
1
General Rule
For a sequence of statements C₁; C₂ and postcondition Q:
wp(C₁; C₂, Q) = wp(C₁, wp(C₂, Q))
We compute the weakest precondition of C₂ first, then use it as the postcondition for C₁
2
Example
Consider this sequence and postcondition:
x := 1; y := x + 1
{y = 2}
3
Computing the VC
wp(x := 1; y := x + 1, y = 2)
  = wp(x := 1, wp(y := x + 1, y = 2))
  = wp(x := 1, (y = 2)[y/x+1])
  = wp(x := 1, x + 1 = 2)
  = (x + 1 = 2)[x/1]
  = 1 + 1 = 2
  = true
VC for If-Else
wp(if B then C₁ else C₂, Q) = (B ⇒ wp(C₁, Q)) ∧ (¬B ⇒ wp(C₂, Q))
Example:
if x > 0 then
  y := 1
else
  y := -1
{y * x > 0}
wp(if x > 0 then y := 1 else y := -1, y * x > 0)
= (x > 0 ⇒ wp(y := 1, y * x > 0)) ∧ 
  (x ≤ 0 ⇒ wp(y := -1, y * x > 0))
= (x > 0 ⇒ 1 * x > 0) ∧ (x ≤ 0 ⇒ -1 * x > 0)
Loop VC Sketch
For a while loop with loop invariant I and postcondition Q:
wp(while b do c, Q) generates these verification conditions:
1
Init: P ⇒ I
Precondition implies invariant
2
Preservation: I ∧ b ⇒ wp(c, I)
Invariant is maintained through each iteration
3
Exit: I ∧ ¬b ⇒ Q
Invariant plus loop termination implies postcondition
Example
For code while b do c with Invariant I and Post-condition Q, we verify the three conditions above
VC Templates Recap
Assignment
Q[x ↦ E]
Sequence
wp(C1, wp(C2, Q))
If
(b ⇒ wp(C1, Q)) ∧ (¬b ⇒ wp(C2, Q))
While
Init ∧ Pres ∧ Exit
Skip
wp(skip, Q) = Q
Exercise: Compute VC
Given the following program and postcondition:
x := 0;
if x < 1 then
    x := x + 1
else
    skip;

Post: x = 1
Question: What's the verification condition (VC) for this program?
Exercise: Compute VC
Let's work backwards using weakest precondition (WP) rules:
1. Start with the postcondition: x = 1

2. For the if-statement (working backwards):
   wp(if x < 1 then x := x + 1 else skip, x = 1)
   = (x < 1 ⇒ wp(x := x + 1, x = 1)) ∧ (x ≥ 1 ⇒ wp(skip, x = 1))
   = (x < 1 ⇒ (x + 1) = 1) ∧ (x ≥ 1 ⇒ x = 1)
   = (x < 1 ⇒ x = 0) ∧ (x ≥ 1 ⇒ x = 1)

3. For the first assignment:
   wp(x := 0, (x < 1 ⇒ x = 0) ∧ (x ≥ 1 ⇒ x = 1))
   = ((0 < 1 ⇒ 0 = 0) ∧ (0 ≥ 1 ⇒ 0 = 1))
   = (true ⇒ true) ∧ (false ⇒ 0 = 1)
   = true ∧ true
   = true

4. Therefore, the verification condition is: true
The VC is true, which means the program will always satisfy its postcondition regardless of the initial state.
What You've Learned
Loop Reasoning
How to reason about loops with invariants
Automated Reasoning
How to automate reasoning with VCG
Logical Formulation
Weakest preconditions as logical formulas
Complete Approach
Verification = logic + automation
What's Next
SMT Solvers
How we solve the verification conditions
Assignment 1
Build a weakest precondition-based verifier for IMP
Continue your journey into automated reasoning with these upcoming topics
Verification Pipeline
The process of generating and solving verification conditions:
Annotated Program
Starting point with pre/post conditions and invariants
Intermediate Verification Language (IVL)
Translation to a verification-friendly representation
Verification Condition Generator (VCG)
Creates logical formulas to verify program correctness
Verification Condition (VC)
Logical formula whose validity implies program correctness
SMT Solver
Automated tool that determines if the VC is valid
Syntax of IMP Language
IMP is a simple imperative programming language used in our verification examples:
Expressions
e ::= n | x | e₁ + e₂ | e₁ - e₂ | e₁ * e₂
Boolean Expressions
b ::= true | false | e₁ = e₂ | e₁ < e₂ | ¬b | b₁ ∧ b₂ | b₁ ∨ b₂
Statements
S ::= skip | x := e | S₁; S₂ | if b then S₁ else S₂ | while b do S
This minimal language includes arithmetic expressions, boolean conditions, and the essential programming constructs needed for verification examples.
Syntax of Guarded Command Language (GCL)
Motivation: Need a loop-free language amendable for VC generation
S ::= skip                     // no operation
    | havoc x                  // nondeterministically assigns any value to x
    | assume b                 // restricts control flow to paths where b holds
    | assert b                 // declares that b must hold (generates VC for b)
    | S ; S                    // sequential composition
    | S ★ S                    // nondeterministic composition
Semantics of Guarded Commands
GC(skip) = assume true
GC(x := e) = assume tmp = x; havoc x; assume (x = e[tmp/x])
GC(c1 ; c2) = GC(c1) ; GC(c2)
GC(c1 ★ c2) = GC(c1) ∧ GC(c2)
GC(if b then c1 else c2) =
  (assume b; GC(c1)) ∧ (assume ¬b; GC(c2))

[Loop rule omitted - will be covered later]
Guarded Command for Assignment
The guarded command translation for an assignment statement:
GC(x := e) = assume tmp = x; havoc x; assume (x = e[tmp/x])
Step-by-step explanation:
  1. First, we temporarily save the old value of x
  1. Then we use havoc to make x's value arbitrary
  1. Finally, we constrain x to equal the expression e with old value of x substituted
This translation handles potential aliasing correctly and allows us to generate precise verification conditions.
Guarded Command for Loop
GC({I} while b do c) =
  assert I;
  havoc x₁; ...; havoc xₙ;   // vars modified in c
  assume I;

  (assume b;
   GC(c);
   assert I;
   assume false)
  ★
  assume ¬b
Better to understand with the control-flow graph
Explanation:
assert I
Check invariant holds before entering loop
havoc ...; assume I
Simulates arbitrary loop iteration
First branch
Executes body once, verifies invariant, then halts
Second branch
Simulates loop exit when condition becomes false
Guarded Command for Loop
Line-by-Line Explanation of Loop VC:
assert I
The loop invariant must hold before the loop starts
havoc x₁; ...; havoc xₙ
Variables modified in body c; "forgotten" to model arbitrary states
assume I
Re-constrain the state to satisfy the invariant after havoc
(assume b; GC(c); assert I; assume false) ★ assume ¬b
Two paths: execute loop body once and verify invariant, or exit loop
assume b / GC(c) / assert I / assume false
First path: assume loop condition, execute body, verify invariant, block further iterations
assume ¬b
Second path: assume loop condition is false (loop exit)
Weakest Precondition (WP) Rules for GC
wp(skip, Q)                = Q
wp(assert C, Q)           = C ∧ Q
wp(assume C, Q)           = C → Q
wp(havoc x, Q)            = ∃a. Q[a/x]    (a is fresh)
wp(S₁; S₂, Q)             = wp(S₁, wp(S₂, Q))
wp(S1 ★ S2, Q)            = wp(S1, Q) ∧ wp(S2, Q)
From IMP to Guarded Commands
{n ≥ 0}
p := 0;
x := 0;
{p = x * m ∧ x ≤ n}
while x < n do
  x := x + 1;
  p := p + m
{p = n * m}

assume p₀ = p; havoc p; assume p = 0;
assume x₀ = x; havoc x; assume x = 0;

assert p = x * m ∧ x ≤ n;  // Check loop invariant initially

havoc x; havoc p;  // Abstract loop execution
assume p = x * m ∧ x ≤ n;  // Assume invariant holds

(assume x < n;  // Loop condition holds
  assume x₁ = x; havoc x; assume x = x₁ + 1;  // x := x + 1
  assume p₁ = p; havoc p; assume p = p₁ + m;  // p := p + m
  assert p = x * m ∧ x ≤ n;  // Invariant preserved
  assume false)  // No fall-through
★
assume ¬(x < n)  // Loop exit condition
Example