CS292C-2: Computer-Aided Reasoning for Software
Lecture 2: IMP Syntax & Semantics
Spring 2025 | Prof. Yu Feng

by Yu Feng

Why Define a Language?
Formal Verification Needs Precision
Verification requires precise semantics to reason about programs.
Real Languages Are Problematic
Too complex, underspecified, or large to prove properties about.
Clean Alternative Needed
IMP (Simple Imperative Programs) provides a simple, well-defined foundation for verification.
The Role of IMP in This Course
Ideal Sandbox
Just expressive enough while remaining simple to analyze.
Turing Complete
Can express any computation despite its minimal design.
Practical Applications
You'll build verifiers, symbolic executors, and synthesizers with it.
Syntax (Recap)
Expressions
e ::= n | x | e1 + e2
   | e1 - e2 | e1 * e2
Booleans
b ::= true | false
 | e1 = e2
 | e1 ≤ e2 | ¬b | b1 ∧ b2
Commands
c ::= skip | x := e 
   | c1 ; c2
   | if b then c1 else c2
   | while b do c
Exercise: Identify Constructs
1
Given Program
while x ≤ 5 do
    x := x + 1;
    y := y * 2
2
Syntax Rules Used
While loop, comparison, assignment, sequence, addition, multiplication
3
Validity Check
Yes, this is valid IMP syntax following the grammar rules.
What is Semantics?
Syntax
Defines how code looks - the structure and form.
Semantics
Defines what code means - the behavior and execution.
Two Approaches
Big-step (results) and small-step (execution traces).
States

Definition
A map from variables to integers.
Example
σ = {x ↦ 2, y ↦ 7}
Notation
σ(x) = 2 and σ[x ↦ 5] = σ' (updated state)
Big-Step Semantics for Expressions

Meaning
⟨e, σ⟩ ⇓ n means: expression e evaluates to n under state σ

Constants
[Const] ⟨n, σ⟩ ⇓ n

Variables
[Var] ⟨x, σ⟩ ⇓ σ(x)

Addition
[Plus] ⟨e1, σ⟩ ⇓ n1, ⟨e2, σ⟩ ⇓ n2 ⇒ ⟨e1 + e2, σ⟩ ⇓ n1 + n2
Example Derivation (Expression)
Evaluating: ⟨x + 1, {x ↦ 2}⟩ ⇓ ?
Derivation tree with Plus rule as root:
            ⟨x + 1, σ⟩ ⇓ 3
            /         \
⟨x, σ⟩ ⇓ 2           ⟨1, σ⟩ ⇓ 1
(by Var rule)        (by Const rule)
The derivation tree shows how the Plus rule (at the root) combines the results of its premises (Var and Const rules) to determine the final evaluation result of 3.
Big-Step Semantics for Commands
⟨c, σ⟩ ⇓ σ' means: running command c in σ produces state σ'
Basic Commands
[Skip] ⟨skip, σ⟩ ⇓ σ
[Assign] ⟨e, σ⟩ ⇓ n ⇒ ⟨x := e, σ⟩ ⇓ σ[x ↦ n]
[Seq] ⟨c1, σ⟩ ⇓ σ1, ⟨c2, σ1⟩ ⇓ σ2 ⇒ ⟨c1; c2, σ⟩ ⇓ σ2
Conditionals
[If-True] ⟨b, σ⟩ ⇓ true, ⟨c1, σ⟩ ⇓ σ' ⇒ ⟨if b then c1 else c2, σ⟩ ⇓ σ'
[If-False] ⟨b, σ⟩ ⇓ false, ⟨c2, σ⟩ ⇓ σ' ⇒ ⟨if b then c1 else c2, σ⟩ ⇓ σ'
Loops
[While-False] ⟨b, σ⟩ ⇓ false ⇒ ⟨while b do c, σ⟩ ⇓ σ
[While-True] ⟨b, σ⟩ ⇓ true, ⟨c, σ⟩ ⇓ σ', ⟨while b do c, σ'⟩ ⇓ σ'' ⇒ ⟨while b do c, σ⟩ ⇓ σ''
Expressions
[Arithmetic] ⟨e1, σ⟩ ⇓ n1, ⟨e2, σ⟩ ⇓ n2 ⇒ ⟨e1 + e2, σ⟩ ⇓ n1 + n2, ⟨e1 - e2, σ⟩ ⇓ n1 - n2, ⟨e1 * e2, σ⟩ ⇓ n1 * n2
[Comparison] ⟨e1, σ⟩ ⇓ n1, ⟨e2, σ⟩ ⇓ n2 ⇒ ⟨e1 = e2, σ⟩ ⇓ (n1 = n2), ⟨e1 ≤ e2, σ⟩ ⇓ (n1 ≤ n2)
[Logic] ⟨b, σ⟩ ⇓ v ⇒ ⟨¬b, σ⟩ ⇓ ¬v and ⟨b1, σ⟩ ⇓ v1, ⟨b2, σ⟩ ⇓ v2 ⇒ ⟨b1 ∧ b2, σ⟩ ⇓ v1 ∧ v2
Example Derivation (Command)
Evaluate: ⟨x := 1; y := x + 2, {}⟩ ⇓ ?
⟨x := 1; y := x + 2, {}⟩ ⇓ {x ↦ 1, y ↦ 3}  (by Seq rule)
├── ⟨x := 1, {}⟩ ⇓ {x ↦ 1}  (by Assign rule)
│   └── ⟨1, {}⟩ ⇓ 1  (by Const rule)
└── ⟨y := x + 2, {x ↦ 1}⟩ ⇓ {x ↦ 1, y ↦ 3}  (by Assign rule)
    └── ⟨x + 2, {x ↦ 1}⟩ ⇓ 3  (by Plus rule)
        ├── ⟨x, {x ↦ 1}⟩ ⇓ 1  (by Var rule)
        └── ⟨2, {x ↦ 1}⟩ ⇓ 2  (by Const rule)
Why Big-Step Semantics?
Direct Reasoning
Enables straightforward reasoning about end results of programs.
Easier Proofs
Simplifies partial correctness proofs in verification.
Limitation
Can't distinguish non-termination from being "stuck" in execution.
Motivation for Small-Step
1
Results vs. Process
Big-step shows what happens, small-step shows how it happens.
3
Key Applications
Symbolic execution, interactive proof assistants, debugging.
∞
Execution Traces
Captures step-by-step program behavior, even for non-terminating programs.
Small-Step Example
1
Initial
(x := 1; x := x + 1, {})
2
Step 1
(skip; x := x + 1, {x ↦ 1})
3
Step 2
(x := x + 1, {x ↦ 1})
4
Final
(skip, {x ↦ 2})
Syntax + Semantics Together
IMP is executable, not just notation
Semantics serves as an interpreter for logic
You'll build symbolic and verification interpreters using this foundation
Exercise: Big-Step Evaluation
Exercise: Loop Tracing
Given σ = {x ↦ 3} and command: while x ≤ 4 do x := x + 1
⟨while x ≤ 4 do x := x + 1, {x ↦ 3}⟩ ⇓ {x ↦ 5}  (by While-True rule)
├── ⟨x ≤ 4, {x ↦ 3}⟩ ⇓ true  (by Leq rule)
│   ├── ⟨x, {x ↦ 3}⟩ ⇓ 3  (by Var rule)
│   └── ⟨4, {x ↦ 3}⟩ ⇓ 4  (by Const rule)
├── ⟨x := x + 1, {x ↦ 3}⟩ ⇓ {x ↦ 4}  (by Assign rule)
│   └── ⟨x + 1, {x ↦ 3}⟩ ⇓ 4  (by Plus rule)
│       ├── ⟨x, {x ↦ 3}⟩ ⇓ 3  (by Var rule)
│       └── ⟨1, {x ↦ 3}⟩ ⇓ 1  (by Const rule)
└── ⟨while x ≤ 4 do x := x + 1, {x ↦ 4}⟩ ⇓ {x ↦ 5}  (by While-True rule)
    ├── ⟨x ≤ 4, {x ↦ 4}⟩ ⇓ true  (by Leq rule)
    │   ├── ⟨x, {x ↦ 4}⟩ ⇓ 4  (by Var rule)
    │   └── ⟨4, {x ↦ 4}⟩ ⇓ 4  (by Const rule)
    ├── ⟨x := x + 1, {x ↦ 4}⟩ ⇓ {x ↦ 5}  (by Assign rule)
    │   └── ⟨x + 1, {x ↦ 4}⟩ ⇓ 5  (by Plus rule)
    │       ├── ⟨x, {x ↦ 4}⟩ ⇓ 4  (by Var rule)
    │       └── ⟨1, {x ↦ 4}⟩ ⇓ 1  (by Const rule)
    └── ⟨while x ≤ 4 do x := x + 1, {x ↦ 5}⟩ ⇓ {x ↦ 5}  (by While-False rule)
        └── ⟨x ≤ 4, {x ↦ 5}⟩ ⇓ false  (by Leq rule)
            ├── ⟨x, {x ↦ 5}⟩ ⇓ 5  (by Var rule)
            └── ⟨4, {x ↦ 5}⟩ ⇓ 4  (by Const rule)
Trace the execution steps manually on whiteboard.
What You've Learned
IMP Purpose
Understanding what IMP is and why it matters for verification.
Formal Definitions
How to formally define a programming language.
Semantic Approaches
Big-step vs. small-step semantics and their applications.
Foundation
Building blocks for everything else in this course.
What's Next

Hoare Logic
Reasoning with Pre/Post Conditions

OCaml
Will be used to implement assignment 1&2

Reading
Slides, reference implementation, Winskel Ch. 2 (optional)