CS292C-3: Computer-Aided Reasoning for Software

CS292C-3: Computer-Aided Reasoning for Software
Welcome to Lecture 3: Hoare Logic I — Reasoning About Programs for Spring 2025. This lecture introduces formal methods for proving program correctness.
YF
by Yu Feng
 
Why Reason Formally About Programs?
Testing
Gives you confidence in your code
Proof
Gives you guarantees about correctness
But what does it mean to "prove" a program correct? We need a logic for reasoning about programs.
Enter: Hoare Logic
{ P } C { Q }
"If P holds before executing C, and C terminates, then Q will hold after."
Origin
Developed by Tony Hoare in 1969
Purpose
Provides a formal system for reasoning about program correctness
Core Concept
Uses "Hoare Triples" to express program specifications
Intuition Behind Hoare Triples
Precondition (P)
What must be true before executing the code
Code (C)
The program statements to execute
Postcondition (Q)
What will be true after execution completes
Example: { x = 1 } x := x + 1 { x = 2 }
What Hoare Logic Can't Do (Yet)
Doesn't Prove Termination
Cannot guarantee that a program will finish executing
Doesn't Check Runtime Errors
No protection against division by zero, null references, etc.
Partial Correctness Only
"If the program terminates, the postcondition holds"
Assignment Rule
The assignment rule in Hoare Logic can be represented as an inference rule:
———————————————
{ Q[x ↦ E] } x := E { Q }
To prove Q holds after x := E, make sure it holds if x were E before the assignment.
1
Substitution
Replace all occurrences of x with E in Q
2
Backward Reasoning
Work backwards from desired postcondition
3
Example
{ x = 1 } x := x + 1 { x = 2 }
Assignment Rule Example
Let's understand the assignment rule with a concrete example:
{ y = 4 } x := 4 { y = x }
To verify this Hoare triple using the assignment rule:
Start with the postcondition: y = x
Substitute all occurrences of x with 4 (the expression being assigned): y = 4
This substitution y = 4 becomes our precondition
The assignment rule is applied as:
{ Q[x ↦ E] } x := E { Q }
{ y = 4 } x := 4 { y = x }
Since our calculated precondition matches the given precondition y = 4, the Hoare triple is valid.
Can You Spot the Invalid Triple?
Triple: { x = 0 } x := x + 1 { x = 0 }
Problem: This triple is invalid. Can you see why?
Correct Precondition: Assignment rule tells us pre should be x + 1 = 0 ⇒ x = -1
Sequence Rule
The sequence rule allows us to compose two Hoare triples:
{ P } C₁ { Q }    { Q } C₂ { R }
────────────────────────────────
        { P } C₁; C₂ { R }
Chain triples using intermediate postcondition Q as the precondition for the next command.
In-Class Derivation Example
Program:
x := 5; y := x + 2

Goal:
{ true } x := 5; y := x + 2 { y = 7 }
Working backward: first apply substitution for each assignment, then connect the parts using the sequence rule.
Annotated Version
Let's solve this step-by-step using a derivation tree:
                          { x+2 = 7 }
                          { x = 5 }
─────────────────────────────────────────── [Assignment]
          { x = 5 } y := x + 2 { y = 7 }
                                                  { 5 = 5 }
                                                  { true }
                                         ─────────────────────────── [Assignment]
                                            { true } x := 5 { x = 5 }
───────────────────────────────────────────────────────────────────────────────────── [Sequence]
                      { true } x := 5; y := x + 2 { y = 7 }
    
Each assertion describes the program state at that point in execution, working backwards from the postcondition to establish the precondition through substitution.
Conditional Rule
{ P ∧ b } C₁ { Q }    { P ∧ ¬b } C₂ { Q }
------------------------------------
{ P } if b then C₁ else C₂ { Q }
Both branches must establish the same postcondition Q from their respective preconditions.
The rule states that if the true branch establishes Q when P and b are true, and the false branch establishes Q when P is true but b is false, then the entire conditional statement establishes Q when P is true.
Conditional Rule Example
Let's apply the conditional rule to prove this Hoare triple:
{true} if x > 0 then y := x else y := −x {y ≥ 0}
Derivation tree:
                 {x > 0}                                       {x ≤ 0}
                 {x ≥ 0}                                       {-x ≥ 0}
       ──────────────────────────── [Assignment]      ────────────────────────────── [Assignment]
       {x > 0} y := x {y ≥ 0}                        {x ≤ 0} y := −x {y ≥ 0}
──────────────────────────────────────────────────────────────────────────────────────── [Conditional]
                {true} if x > 0 then y := x else y := −x {y ≥ 0}
The derivation shows how both branches establish the postcondition {y ≥ 0} from their respective preconditions, validating the entire conditional statement.
Skip Rule
The skip command does nothing — it's the "no-op" of programming languages.
——————————
{ P } skip { P }
Since the skip command doesn't change any variables, whatever condition was true before execution remains true after.
Intuition
Makes sense — doing nothing preserves the state.
Applications
Useful in proofs with empty code blocks or as placeholders in conditional branches.
Is the following Hoare triple valid? Why or why not?
{ z = 2 } y := x { y = x }
Strengthening & Weakening
Strengthen Precondition
P' ⇒ P    { P } C { Q }
─────────────────────
      { P' } C { Q }
Making precondition stronger (more specific) is valid.
Weaken Postcondition
{ P } C { Q }    Q ⇒ Q'
─────────────────────
      { P } C { Q' }
Making postcondition weaker (less specific) is valid.
These principles are useful for composing derivations!
A Simple Example
Let's derive: { z = 2 } y := x { y = x }
Step 1: Identify Goal
Prove { z = 2 } y := x { y = x }
Step 2: Apply Assignment Rule
Working backward: { y = x[y ↦ x] } simplifies to { x = x }
Step 3: Verify Precondition
Check { z = 2 } ⇒ { x = x }. Since { x = x } is a tautology, any precondition implies it.
Derivation tree:
                  (always true)
                    { x = x }
─────────────────────────────────── [Assignment Rule]
        { x = x } y := x { y = x }
─────────────────────────────────── [Strengthening Precondition]
        { z = 2 } y := x { y = x }
    
Note: { z = 2 } is stronger than the minimal precondition { x = x }, demonstrating precondition strengthening while maintaining validity.
Exercise 1 (Try it Yourself)
Problem
{ x = 3 } x := x + 1; y := x { y = 4 }
Question 1
What is the intermediate assertion?
Question 2
What rule(s) apply?
Common Pitfalls
Forgetting Substitution
Always apply the substitution rule correctly
Skipping Intermediate Assertions
Each step needs a proper assertion
Misapplying Assignment Rule
Remember it works backwards from postcondition
We'll train your logic muscles 💪
Theorem: Soundness & Completeness
We use two important notations for Hoare triples:
⊨ {P} S {Q}: The triple is valid (true semantically)
⊢ {P} S {Q}: The triple is provable in our proof system
If ⊢ { P } C { Q }, then { P } C { Q } is true with respect to big-step semantics
Soundness: If we can prove a triple (⊢ {P} S {Q}), then it is valid (⊨ {P} S {Q})
Completeness: If a triple is valid (⊨ {P} S {Q}), then we can prove it (⊢ {P} S {Q})
Connection to Semantics
IMP Semantics
Hoare Logic is based on formal language semantics
State Transitions
⟨C, σ⟩ ⇓ σ' describes how programs change state
Correctness
σ ⊨ P ⇒ σ' ⊨ Q ensures postconditions hold
Soundness
Triples must be consistent with semantics
Hoare Logic in the Wild
Verified Kernels
seL4 microkernel uses formal verification to guarantee security properties and eliminate entire classes of bugs.
Smart Contract Verification
Formal methods prevent costly vulnerabilities in blockchain applications where code is immutable after deployment.
Industrial Tools
Why3, Dafny, Viper, and Frama-C implement Hoare Logic principles to verify real-world software systems.
Foundation for Modern Verification
These applications build directly on the same concepts you're learning in this course.
What's Next
Hoare Logic II: Loops and Invariants
Assignment 1 is coming soon
You'll build your own Hoare triple checker for IMP!