微信客服：xiaoxionga100
微信客服：ITCS521
COMP2111-comp2111代写
时间：2023-04-13
COMP2111 Week 8
Term 1, 2023
Hoare Logic
1
Sir Tony Hoare
Pioneer in formal verification
Invented: Quicksort,
the null reference (called it his “billion dollar mistake”)
CSP (formal specification language), and
Hoare Logic
2
Summary
L: A simple imperative programming language
Hoare triples (SYNTAX)
Hoare logic (PROOF)
Semantics for Hoare logic
3
Summary
L: A simple imperative programming language
Hoare triples (SYNTAX)
Hoare logic (PROOF)
Semantics for Hoare logic
4
Imperative Programming
impero¯
Definition
Imperative programming is where programs are described as a
series of statements or commands to manipulate mutable state or
cause externally observable effects.
States may take the form of a mapping from variable names to
their values, or even a model of a CPU state with a memory model
(for example, in an assembly language).
5
L: A simple imperative programming language
Consider the vocabulary of basic arithmetic:
Constant symbols: 0, 1, 2, . . .
Function symbols: +, ∗, . . .
Predicate symbols: <,≤,≥, |, . . .
An (arithmetic) expression is a term over this vocabulary.
A boolean expression is a predicate formula over this
vocabulary.
6
L: A simple imperative programming language
Consider the vocabulary of basic arithmetic:
Constant symbols: 0, 1, 2, . . .
Function symbols: +, ∗, . . .
Predicate symbols: <,≤,≥, |, . . .
An (arithmetic) expression is a term over this vocabulary.
A boolean expression is a predicate formula over this
vocabulary.
7
L: A simple imperative programming language
Consider the vocabulary of basic arithmetic:
Constant symbols: 0, 1, 2, . . .
Function symbols: +, ∗, . . .
Predicate symbols: <,≤,≥, |, . . .
An (arithmetic) expression is a term over this vocabulary.
A boolean expression is a predicate formula over this
vocabulary.
8
The language L
The language L is a simple imperative programming language
made up of four statements:
Assignment: x :=e
where x is a variable and e is an arithmetic
expression.
Sequencing: P;Q
Conditional: if g then P else Q fi
where g is a boolean expression.
While: while g do P od
9
The language L
The language L is a simple imperative programming language
made up of four statements:
Assignment: x :=e
where x is a variable and e is an arithmetic
expression.
Sequencing: P;Q
Conditional: if g then P else Q fi
where g is a boolean expression.
While: while g do P od
10
The language L
The language L is a simple imperative programming language
made up of four statements:
Assignment: x :=e
where x is a variable and e is an arithmetic
expression.
Sequencing: P;Q
Conditional: if g then P else Q fi
where g is a boolean expression.
While: while g do P od
11
The language L
The language L is a simple imperative programming language
made up of four statements:
Assignment: x :=e
where x is a variable and e is an arithmetic
expression.
Sequencing: P;Q
Conditional: if g then P else Q fi
where g is a boolean expression.
While: while g do P od
12
Factorial in L
Example
i := 0;
m := 1;
while i < N do
i := i + 1;
m := m ∗ i
od
13
Summary
L: A simple imperative programming language
Hoare triples (SYNTAX)
Hoare logic (PROOF)
Semantics for Hoare logic
14
Summary
L: A simple imperative programming language
Hoare triples (SYNTAX)
Hoare logic (PROOF)
Semantics for Hoare logic
15
Hoare Logic
We are going to define what’s called a Hoare Logic for L to allow
us to prove properties of our program.
We write a Hoare triple judgement as:
{ϕ} P {ψ}
Where ϕ and ψ are logical formulae about states, called assertions,
and P is a program. This triple states that if the program P
terminates and it successfully evaluates from a starting state
satisfying the precondition ϕ, then the result state will satisfy the
postcondition ψ.
16
Hoare triple: Examples
Example
{(x = 0)} x := 1 {(x = 1)}
{(x = 499)} x := x + 1 {(x = 500)}
{(x > 0)} y := 0− x {(y < 0) ∧ (x 6= y)}
17
Hoare triple: Examples
Example
{(x = 0)} x := 1 {(x = 1)}
{(x = 499)} x := x + 1 {(x = 500)}
{(x > 0)} y := 0− x {(y < 0) ∧ (x 6= y)}
18
Hoare triple: Examples
Example
{(x = 0)} x := 1 {(x = 1)}
{(x = 499)} x := x + 1 {(x = 500)}
{(x > 0)} y := 0− x {(y < 0) ∧ (x 6= y)}
19
Hoare triple: Factorial Examples
Example
{N ≥ 0}
i := 0;
m := 1;
while i < N do
i := i + 1;
m := m ∗ i
od
{m = N!}
20
Summary
L: A simple imperative programming language
Hoare triples (SYNTAX)
Hoare logic (PROOF)
Semantics for Hoare logic
21
Motivation
Question
We know what we want informally; how do we establish when a
triple is valid?
Develop a semantics, OR
Derive the triple in a syntactic manner (i.e. Hoare proof)
Hoare logic consists of one axiom and four inference rules for
deriving Hoare triples.
22
Motivation
Question
We know what we want informally; how do we establish when a
triple is valid?
Develop a semantics, OR
Derive the triple in a syntactic manner (i.e. Hoare proof)
Hoare logic consists of one axiom and four inference rules for
deriving Hoare triples.
23
Motivation
Question
We know what we want informally; how do we establish when a
triple is valid?
Develop a semantics, OR
Derive the triple in a syntactic manner (i.e. Hoare proof)
Hoare logic consists of one axiom and four inference rules for
deriving Hoare triples.
24
Assignment
(assign){ϕ[e/x ]} x := e {ϕ}
Intuition:
If x has property ϕ after executing the assignment; then e must
have property ϕ before executing the assignment
25
Assignment: Example
Example
{(y = 0)} x := y {(x = 0)}
{
(y = y)
} x := y {(x = y)}
{
(1 < 2)
} x := 1 {(x < 2)}
{(y = 3)} x := y {(x > 2)}
Problem!
26
Assignment: Example
Example
{(y = 0)} x := y {(x = 0)}
{
(y = y)
} x := y {(x = y)}
{
(1 < 2)
} x := 1 {(x < 2)}
{(y = 3)} x := y {(x > 2)}
Problem!
27
Assignment: Example
Example
{(y = 0)} x := y {(x = 0)}
{(y = y)} x := y {(x = y)}
{
(1 < 2)
} x := 1 {(x < 2)}
{(y = 3)} x := y {(x > 2)}
Problem!
28
Assignment: Example
Example
{(y = 0)} x := y {(x = 0)}
{(y = y)} x := y {(x = y)}
{
(1 < 2)
} x := 1 {(x < 2)}
{(y = 3)} x := y {(x > 2)}
Problem!
29
Assignment: Example
Example
{(y = 0)} x := y {(x = 0)}
{(y = y)} x := y {(x = y)}
{(1 < 2)} x := 1 {(x < 2)}
{(y = 3)} x := y {(x > 2)}
Problem!
30
Assignment: Example
Example
{(y = 0)} x := y {(x = 0)}
{(y = y)} x := y {(x = y)}
{(1 < 2)} x := 1 {(x < 2)}
{(y = 3)} x := y {(x > 2)} Problem!
31
Sequence
{ϕ}P {ψ} {ψ}Q {ρ}
(seq){ϕ}P;Q {ρ}
Intuition:
If the postcondition of P matches the precondition of Q we can
sequentially combine the two program fragments
32
Sequence: Example
Example
{
(0 = 0)
} x := 0 {
(x = 0)
} {
(x = 0)
} y := 0 {(x = y)}
(seq){
(0 = 0)
} x := 0; y := 0 {(x = y)}
33
Sequence: Example
Example
{
(0 = 0)
} x := 0 {(x = 0)} {(x = 0)} y := 0 {(x = y)}
(seq){
(0 = 0)
} x := 0; y := 0 {(x = y)}
34
Sequence: Example
Example
{(0 = 0)} x := 0 {(x = 0)} {(x = 0)} y := 0 {(x = y)}
(seq){(0 = 0)} x := 0; y := 0 {(x = y)}
35
Conditional
{ϕ ∧ g}P {ψ} {ϕ ∧ ¬g}Q {ψ}
(if){ϕ} if g then P else Q fi {ψ}
Intuition:
When a conditional is executed, either P or Q will be
executed.
If ψ is a postcondition of the conditional, then it must be a
postcondition of both branches
Likewise, if ϕ is a precondition of the conditional, then it must
be a precondition of both branches
Which branch gets executed depends on g , so we can assume
g to be a precondition of P and ¬g to be a precondition of Q.
36
While
{ϕ ∧ g}P {ϕ}
(loop){ϕ}while g do P od {ϕ ∧ ¬g}
Intuition:
ϕ is a loop invariant. It must be both a pre- and
postcondition of P, so that sequences of Ps can be run
together.
If the while loop terminates, g cannot hold.
37
Consequence
There is one more rule, called the rule of consequence, that we
need to insert ordinary logical reasoning into our Hoare logic
proofs:
ϕ′ → ϕ {ϕ}P {ψ} ψ → ψ′
(cons){ϕ′}P {ψ′}
Intuition:
Adding assertions to the precondition makes it more likely the
postcondition will be reached
Removing assertions from the postcondition makes it more
likely the postcondition will be reached
If you can reach the postcondition initially, then you can reach
it in the more likely scenario
38
Consequence
There is one more rule, called the rule of consequence, that we
need to insert ordinary logical reasoning into our Hoare logic
proofs:
ϕ′ → ϕ {ϕ}P {ψ} ψ → ψ′
(cons){ϕ′}P {ψ′}
Intuition:
Adding assertions to the precondition makes it more likely the
postcondition will be reached
Removing assertions from the postcondition makes it more
likely the postcondition will be reached
If you can reach the postcondition initially, then you can reach
it in the more likely scenario
39
Back to Assignment Example
Example
{(y = 3)} x := y {(x > 2)} Problem!
{(y = 3)}x := y{(x > 2)}(assign, cons)
{(y > 2)}x := y{(x > 2)}(assign)
40
Back to Assignment Example
Example
{(y = 3)} x := y {(x > 2)} Problem!
{(y = 3)}x := y{(x > 2)}(assign, cons)
{(y > 2)}x := y{(x > 2)}(assign)
41
Back to Assignment Example
Example
{(y = 3)} x := y {(x > 2)} Problem!
{(y = 3)}x := y{(x > 2)}(assign, cons)
{(y > 2)}x := y{(x > 2)}(assign)
42
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{N ≥ 0}
{1 = 0! ∧ N ≥ 0}
i := 0;
{1 = i ! ∧ N ≥ 0}
{1 = i ! ∧ N ≥ 0}
m := 1;
{m = i ! ∧ N ≥ 0}
{m = i ! ∧ N ≥ 0}
while i < N do
{m = i ! ∧ N ≥ 0 ∧ i < N}
{m × (i + 1) = (i + 1)! ∧ N ≥ 0}
i := i + 1;
{m × i = i ! ∧ N ≥ 0}
m := m × i
{m = i ! ∧ N ≥ 0}
od
{m = i ! ∧ N ≥ 0 ∧ i = N}
{m = N!}
{ϕ ∧ g} P {ψ} {ϕ ∧ ¬g} Q {ψ}
{ϕ} if g then P else Q fi {ψ}
{ϕ[x := e]} x := e {ϕ}
{ϕ ∧ g} P {ϕ}
{ϕ} while g do P od {ϕ ∧ ¬g}
{ϕ} P {α} {α} Q {ψ}
{ϕ} P;Q {ψ}
ϕ′ ⇒ ϕ {ϕ} P {ψ} ψ ⇒ ψ′
{ϕ′} P {ψ′}
note: (i + 1)! = i!× (i + 1)
43
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{N ≥ 0}
{1 = 0! ∧ N ≥ 0}
i := 0;
{1 = i ! ∧ N ≥ 0}
{1 = i ! ∧ N ≥ 0}
m := 1;
{m = i ! ∧ N ≥ 0}
{m = i ! ∧ N ≥ 0}
while i < N do
{m = i ! ∧ N ≥ 0 ∧ i < N}
{m × (i + 1) = (i + 1)! ∧ N ≥ 0}
i := i + 1;
{m × i = i ! ∧ N ≥ 0}
m := m × i
{m = i ! ∧ N ≥ 0}
od {m = i ! ∧ N ≥ 0 ∧ i = N}
{m = N!}
{ϕ ∧ g} P {ψ} {ϕ ∧ ¬g} Q {ψ}
{ϕ} if g then P else Q fi {ψ}
{ϕ[x := e]} x := e {ϕ}
{ϕ ∧ g} P {ϕ}
{ϕ} while g do P od {ϕ ∧ ¬g}
{ϕ} P {α} {α} Q {ψ}
{ϕ} P;Q {ψ}
ϕ′ ⇒ ϕ {ϕ} P {ψ} ψ ⇒ ψ′
{ϕ′} P {ψ′}
note: (i + 1)! = i!× (i + 1)
44
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{N ≥ 0}
{1 = 0! ∧ N ≥ 0}
i := 0;
{1 = i ! ∧ N ≥ 0}
{1 = i ! ∧ N ≥ 0}
m := 1;
{m = i ! ∧ N ≥ 0}
{m = i ! ∧ N ≥ 0}
while i < N do
{m = i ! ∧ N ≥ 0 ∧ i < N}
{m × (i + 1) = (i + 1)! ∧ N ≥ 0}
i := i + 1;
{m × i = i ! ∧ N ≥ 0}
m := m × i
{m = i ! ∧ N ≥ 0}
od {m = i ! ∧ N ≥ 0 ∧ i = N}
{m = N!}
{ϕ ∧ g} P {ψ} {ϕ ∧ ¬g} Q {ψ}
{ϕ} if g then P else Q fi {ψ}
{ϕ[x := e]} x := e {ϕ}
{ϕ ∧ g} P {ϕ}
{ϕ} while g do P od {ϕ ∧ ¬g}
{ϕ} P {α} {α} Q {ψ}
{ϕ} P;Q {ψ}
ϕ′ ⇒ ϕ {ϕ} P {ψ} ψ ⇒ ψ′
{ϕ′} P {ψ′}
note: (i + 1)! = i!× (i + 1)
45
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{N ≥ 0}
{1 = 0! ∧ N ≥ 0}
i := 0;
{1 = i ! ∧ N ≥ 0}
{1 = i ! ∧ N ≥ 0}
m := 1;
{m = i ! ∧ N ≥ 0}
{m = i ! ∧ N ≥ 0}
while i < N do
{m = i ! ∧ N ≥ 0 ∧ i < N}
{m × (i + 1) = (i + 1)! ∧ N ≥ 0}
i := i + 1;
{m × i = i ! ∧ N ≥ 0}
m := m × i
{m = i ! ∧ N ≥ 0}
od {m = i ! ∧ N ≥ 0 ∧ i = N}
{m = N!}
{ϕ ∧ g} P {ψ} {ϕ ∧ ¬g} Q {ψ}
{ϕ} if g then P else Q fi {ψ}
{ϕ[x := e]} x := e {ϕ}
{ϕ ∧ g} P {ϕ}
{ϕ} while g do P od {ϕ ∧ ¬g}
{ϕ} P {α} {α} Q {ψ}
{ϕ} P;Q {ψ}
ϕ′ ⇒ ϕ {ϕ} P {ψ} ψ ⇒ ψ′
{ϕ′} P {ψ′}
note: (i + 1)! = i!× (i + 1)
46
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{N ≥ 0}
{1 = 0! ∧ N ≥ 0}
i := 0;
{1 = i ! ∧ N ≥ 0}
{1 = i ! ∧ N ≥ 0}
m := 1;
{m = i ! ∧ N ≥ 0}
{m = i ! ∧ N ≥ 0}
while i < N do {m = i ! ∧ N ≥ 0 ∧ i < N}
{m × (i + 1) = (i + 1)! ∧ N ≥ 0}
i := i + 1;
{m × i = i ! ∧ N ≥ 0}
m := m × i
{m = i ! ∧ N ≥ 0}
od {m = i ! ∧ N ≥ 0 ∧ i = N}
{m = N!}
{ϕ ∧ g} P {ψ} {ϕ ∧ ¬g} Q {ψ}
{ϕ} if g then P else Q fi {ψ}
{ϕ[x := e]} x := e {ϕ}
{ϕ ∧ g} P {ϕ}
{ϕ} while g do P od {ϕ ∧ ¬g}
{ϕ} P {α} {α} Q {ψ}
{ϕ} P;Q {ψ}
ϕ′ ⇒ ϕ {ϕ} P {ψ} ψ ⇒ ψ′
{ϕ′} P {ψ′}
note: (i + 1)! = i!× (i + 1)
47
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{N ≥ 0}
{1 = 0! ∧ N ≥ 0}
i := 0;
{1 = i ! ∧ N ≥ 0}
{1 = i ! ∧ N ≥ 0}
m := 1;
{m = i ! ∧ N ≥ 0}
{m = i ! ∧ N ≥ 0}
while i < N do {m = i ! ∧ N ≥ 0 ∧ i < N}
{m × (i + 1) = (i + 1)! ∧ N ≥ 0}
i := i + 1;
{m × i = i ! ∧ N ≥ 0}
m := m × i
{m = i ! ∧ N ≥ 0}
od {m = i ! ∧ N ≥ 0 ∧ i = N}
{m = N!}
{ϕ ∧ g} P {ψ} {ϕ ∧ ¬g} Q {ψ}
{ϕ} if g then P else Q fi {ψ}
{ϕ[x := e]} x := e {ϕ}
{ϕ ∧ g} P {ϕ}
{ϕ} while g do P od {ϕ ∧ ¬g}
{ϕ} P {α} {α} Q {ψ}
{ϕ} P;Q {ψ}
ϕ′ ⇒ ϕ {ϕ} P {ψ} ψ ⇒ ψ′
{ϕ′} P {ψ′}
note: (i + 1)! = i!× (i + 1)
48
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{N ≥ 0}
{1 = 0! ∧ N ≥ 0}
i := 0;
{1 = i ! ∧ N ≥ 0}
{1 = i ! ∧ N ≥ 0}
m := 1;
{m = i ! ∧ N ≥ 0}
{m = i ! ∧ N ≥ 0}
while i < N do {m = i ! ∧ N ≥ 0 ∧ i < N}
{m × (i + 1) = (i + 1)! ∧ N ≥ 0}
i := i + 1;
{m × i = i ! ∧ N ≥ 0}
m := m × i
{m = i ! ∧ N ≥ 0}
od {m = i ! ∧ N ≥ 0 ∧ i = N}
{m = N!}
{ϕ ∧ g} P {ψ} {ϕ ∧ ¬g} Q {ψ}
{ϕ} if g then P else Q fi {ψ}
{ϕ[x := e]} x := e {ϕ}
{ϕ ∧ g} P {ϕ}
{ϕ} while g do P od {ϕ ∧ ¬g}
{ϕ} P {α} {α} Q {ψ}
{ϕ} P;Q {ψ}
ϕ′ ⇒ ϕ {ϕ} P {ψ} ψ ⇒ ψ′
{ϕ′} P {ψ′}
note: (i + 1)! = i!× (i + 1)
49
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{N ≥ 0}
{1 = 0! ∧ N ≥ 0}
i := 0;
{1 = i ! ∧ N ≥ 0}
{1 = i ! ∧ N ≥ 0}
m := 1;
{m = i ! ∧ N ≥ 0}
{m = i ! ∧ N ≥ 0}
while i < N do {m = i ! ∧ N ≥ 0 ∧ i < N}
{m × (i + 1) = (i + 1)! ∧ N ≥ 0}
i := i + 1;
{m × i = i ! ∧ N ≥ 0}
m := m × i
{m = i ! ∧ N ≥ 0}
od {m = i ! ∧ N ≥ 0 ∧ i = N}
{m = N!}
{ϕ ∧ g} P {ψ} {ϕ ∧ ¬g} Q {ψ}
{ϕ} if g then P else Q fi {ψ}
{ϕ[x := e]} x := e {ϕ}
{ϕ ∧ g} P {ϕ}
{ϕ} while g do P od {ϕ ∧ ¬g}
{ϕ} P {α} {α} Q {ψ}
{ϕ} P;Q {ψ}
ϕ′ ⇒ ϕ {ϕ} P {ψ} ψ ⇒ ψ′
{ϕ′} P {ψ′}
note: (i + 1)! = i!× (i + 1)
50
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{N ≥ 0}
{1 = 0! ∧ N ≥ 0}
i := 0;
{1 = i ! ∧ N ≥ 0}
{1 = i ! ∧ N ≥ 0}
m := 1;{m = i ! ∧ N ≥ 0}
{m = i ! ∧ N ≥ 0}
while i < N do {m = i ! ∧ N ≥ 0 ∧ i < N}
{m × (i + 1) = (i + 1)! ∧ N ≥ 0}
i := i + 1;
{m × i = i ! ∧ N ≥ 0}
m := m × i
{m = i ! ∧ N ≥ 0}
od {m = i ! ∧ N ≥ 0 ∧ i = N}
{m = N!}
{ϕ ∧ g} P {ψ} {ϕ ∧ ¬g} Q {ψ}
{ϕ} if g then P else Q fi {ψ}
{ϕ[x := e]} x := e {ϕ}
{ϕ ∧ g} P {ϕ}
{ϕ} while g do P od {ϕ ∧ ¬g}
{ϕ} P {α} {α} Q {ψ}
{ϕ} P;Q {ψ}
ϕ′ ⇒ ϕ {ϕ} P {ψ} ψ ⇒ ψ′
{ϕ′} P {ψ′}
note: (i + 1)! = i!× (i + 1)
51
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{N ≥ 0}
{1 = 0! ∧ N ≥ 0}
i := 0;
{1 = i ! ∧ N ≥ 0}
{1 = i ! ∧ N ≥ 0}m := 1;{m = i ! ∧ N ≥ 0}
{m = i ! ∧ N ≥ 0}
while i < N do {m = i ! ∧ N ≥ 0 ∧ i < N}
{m × (i + 1) = (i + 1)! ∧ N ≥ 0}
i := i + 1;
{m × i = i ! ∧ N ≥ 0}
m := m × i
{m = i ! ∧ N ≥ 0}
od {m = i ! ∧ N ≥ 0 ∧ i = N}
{m = N!}
{ϕ ∧ g} P {ψ} {ϕ ∧ ¬g} Q {ψ}
{ϕ} if g then P else Q fi {ψ}
{ϕ[x := e]} x := e {ϕ}
{ϕ ∧ g} P {ϕ}
{ϕ} while g do P od {ϕ ∧ ¬g}
{ϕ} P {α} {α} Q {ψ}
{ϕ} P;Q {ψ}
ϕ′ ⇒ ϕ {ϕ} P {ψ} ψ ⇒ ψ′
{ϕ′} P {ψ′}
note: (i + 1)! = i!× (i + 1)
52
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{N ≥ 0}
{1 = 0! ∧ N ≥ 0}
i := 0;{1 = i ! ∧ N ≥ 0}
{1 = i ! ∧ N ≥ 0}m := 1;{m = i ! ∧ N ≥ 0}
{m = i ! ∧ N ≥ 0}
while i < N do {m = i ! ∧ N ≥ 0 ∧ i < N}
{m × (i + 1) = (i + 1)! ∧ N ≥ 0}
i := i + 1;
{m × i = i ! ∧ N ≥ 0}
m := m × i
{m = i ! ∧ N ≥ 0}
od {m = i ! ∧ N ≥ 0 ∧ i = N}
{m = N!}
{ϕ ∧ g} P {ψ} {ϕ ∧ ¬g} Q {ψ}
{ϕ} if g then P else Q fi {ψ}
{ϕ[x := e]} x := e {ϕ}
{ϕ ∧ g} P {ϕ}
{ϕ} while g do P od {ϕ ∧ ¬g}
{ϕ} P {α} {α} Q {ψ}
{ϕ} P;Q {ψ}
ϕ′ ⇒ ϕ {ϕ} P {ψ} ψ ⇒ ψ′
{ϕ′} P {ψ′}
note: (i + 1)! = i!× (i + 1)
53
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{N ≥ 0}
{1 = 0! ∧ N ≥ 0} i := 0;{1 = i ! ∧ N ≥ 0}
{1 = i ! ∧ N ≥ 0}m := 1;{m = i ! ∧ N ≥ 0}
{m = i ! ∧ N ≥ 0}
while i < N do {m = i ! ∧ N ≥ 0 ∧ i < N}
{m × (i + 1) = (i + 1)! ∧ N ≥ 0}
i := i + 1;
{m × i = i ! ∧ N ≥ 0}
m := m × i
{m = i ! ∧ N ≥ 0}
od {m = i ! ∧ N ≥ 0 ∧ i = N}
{m = N!}
{ϕ ∧ g} P {ψ} {ϕ ∧ ¬g} Q {ψ}
{ϕ} if g then P else Q fi {ψ}
{ϕ[x := e]} x := e {ϕ}
{ϕ ∧ g} P {ϕ}
{ϕ} while g do P od {ϕ ∧ ¬g}
{ϕ} P {α} {α} Q {ψ}
{ϕ} P;Q {ψ}
ϕ′ ⇒ ϕ {ϕ} P {ψ} ψ ⇒ ψ′
{ϕ′} P {ψ′}
note: (i + 1)! = i!× (i + 1)
54
Practice Exercise
Example
m := 1;
n := 1;
i := 1;
while i < N do
t := m;
m := n;
n := m + t;
i := i + 1
od
What does this L program P compute?
What is a valid Hoare triple {ϕ}P{ψ} of this program?
Prove using the inference rules and consequence axiom that
this Hoare triple is valid.
55
Practice Exercise
Example
m := 1;
n := 1;
i := 1;
while i < N do
t := m;
m := n;
n := m + t;
i := i + 1
od
What does this L program P compute?
What is a valid Hoare triple {ϕ}P{ψ} of this program?
Prove using the inference rules and consequence axiom that
this Hoare triple is valid.
56
Summary
L: A simple imperative programming language
Hoare triples (SYNTAX)
Hoare logic (PROOF)
Semantics for Hoare logic
57
Recall
If R and S are binary relations, then the relational composition
of R and S , R; S is the relation:
R;S := {(a, c) : ∃b such that (a, b) ∈ R and (b, c) ∈ S}
If R ⊆ A× B is a relation, and X ⊆ A, then the image of X
under R, R(X ) is the subset of B defined as:
R(X ) := {b ∈ B : ∃a inX such that (a, b) ∈ R}.
58
Informal semantics
Hoare logic gives a proof of {ϕ}P {ψ}, that is: ` {ϕ}P {ψ}
(axiomatic semantics)
How do we determine when {ϕ}P {ψ} is valid, that is:
|= {ϕ}P {ψ}?
If ϕ holds in a state of some computational model
then ψ holds in the state reached after a successful execution of P.
59
Informal semantics
Hoare logic gives a proof of {ϕ}P {ψ}, that is: ` {ϕ}P {ψ}
(axiomatic semantics)
How do we determine when {ϕ}P {ψ} is valid, that is:
|= {ϕ}P {ψ}?
If ϕ holds in a state of some computational model
then ψ holds in the state reached after a successful execution of P.
60
Informal semantics: Programs
What is a program?
A
partial
function mapping system states to system states
61
Informal semantics: Programs
What is a program?
A
partial
function mapping system states to system states
62
Informal semantics: Programs
What is a program?
A partial function mapping system states to system states
63
Informal semantics: Programs
What is a program?
A relation between system states
64
Informal semantics: States
What is a state of a computational model?
Two approaches:
Concrete: from a physical perspective
States are memory configurations, register contents, etc.
Store of variables and the values associated with them
Abstract: from a mathematical perspective
The pre-/postcondition predicates hold in a state
⇒ States are logical interpretations (Model + Environment)
There is only one model of interest: standard interpretations of
arithmetical symbols
⇒ States are fully determined by environments
⇒ States are functions that map variables to values
65
Informal semantics: States
What is a state of a computational model?
Two approaches:
Concrete: from a physical perspective
States are memory configurations, register contents, etc.
Store of variables and the values associated with them
Abstract: from a mathematical perspective
The pre-/postcondition predicates hold in a state
⇒ States are logical interpretations (Model + Environment)
There is only one model of interest: standard interpretations of
arithmetical symbols
⇒ States are fully determined by environments
⇒ States are functions that map variables to values
66
Informal semantics: States
What is a state of a computational model?
Two approaches:
Concrete: from a physical perspective
States are memory configurations, register contents, etc.
Store of variables and the values associated with them
Abstract: from a mathematical perspective
The pre-/postcondition predicates hold in a state
⇒ States are logical interpretations (Model + Environment)
There is only one model of interest: standard interpretations of
arithmetical symbols
⇒ States are fully determined by environments
⇒ States are functions that map variables to values
67
Informal semantics: States
What is a state of a computational model?
Two approaches:
Concrete: from a physical perspective
States are memory configurations, register contents, etc.
Store of variables and the values associated with them
Abstract: from a mathematical perspective
The pre-/postcondition predicates hold in a state
⇒ States are logical interpretations (Model + Environment)
There is only one model of interest: standard interpretations of
arithmetical symbols
⇒ States are fully determined by environments
⇒ States are functions that map variables to values
68
Informal semantics: States
What is a state of a computational model?
Two approaches:
Concrete: from a physical perspective
States are memory configurations, register contents, etc.
Store of variables and the values associated with them
Abstract: from a mathematical perspective
The pre-/postcondition predicates hold in a state
⇒ States are logical interpretations (Model + Environment)
There is only one model of interest: standard interpretations of
arithmetical symbols
⇒ States are fully determined by environments
⇒ States are functions that map variables to values
69
Informal semantics: States
What is a state of a computational model?
Two approaches:
Concrete: from a physical perspective
States are memory configurations, register contents, etc.
Store of variables and the values associated with them
Abstract: from a mathematical perspective
The pre-/postcondition predicates hold in a state
⇒ States are logical interpretations (Model + Environment)
There is only one model of interest: standard interpretations of
arithmetical symbols
⇒ States are fully determined by environments
⇒ States are functions that map variables to values
70
Informal semantics: States
and Programs
State space (Env)
x ← 1
y ← 1
z ← 2
x ← 0
y ← 0
z ← 0
x ← 0
y ← 1
z ← 2
x ← 3
y ← 2
z ← 1
x ← 0
y ← 1
z ← 0
x ← 1
y ← 1
z ← 1 x ← 2
y ← 2
z ← 2
71
Informal semantics: States and Programs
State space (Env)
x ← 1
y ← 1
z ← 2
x ← 0
y ← 0
z ← 0
x ← 0
y ← 1
z ← 2
x ← 3
y ← 2
z ← 1
x ← 0
y ← 1
z ← 0
x ← 1
y ← 1
z ← 1 x ← 2
y ← 2
z ← 2
72
Informal semantics: States and Programs
73
Semantics for L
An environment or state is a function from variables to numeric
values. We denote by Env the set of all environments.
NB
An environment, η, assigns a numeric value [[e]]η to all expressions
e, and a boolean value [[b]]η to all boolean expressions b.
Given a program P of L, we define [[P]] to be a binary relation on
Env in the following manner...
74
Semantics for L
An environment or state is a function from variables to numeric
values. We denote by Env the set of all environments.
NB
An environment, η, assigns a numeric value [[e]]η to all expressions
e, and a boolean value [[b]]η to all boolean expressions b.
Given a program P of L, we define [[P]] to be a binary relation on
Env in the following manner...
75
Assignment
(η, η′) ∈ [[x := e]] if, and only if η′ = η[x 7→ [[e]]η]
76
Assignment: [[z := 2]]
State space (Env)
x ← 1
y ← 1
z ← 2
x ← 0
y ← 0
z ← 0
x ← 0
y ← 1
z ← 2
x ← 3
y ← 2
z ← 1
x ← 0
y ← 1
z ← 0
x ← 1
y ← 1
z ← 1 x ← 2
y ← 2
z ← 2
77
Sequencing
[[P;Q]] = [[P]]; [[Q]]
where, on the RHS, ; is relational composition.
78
Conditional, first attempt
[[if b then P else Q fi]] =
{
[[P]] if [[b]]η = true
[[Q]] otherwise.
79
Detour: Predicates as programs
A boolean expression b defines a subset (or unary relation) of Env:
〈b〉 = {η : [[b]]η = true}
This can be extended to a binary relation (i.e. a program):
[[b]] = {(η, η) : η ∈ 〈b〉}
Intuitively, b corresponds to the program
if b then skip else ⊥ fi
80
Detour: Predicates as programs
A boolean expression b defines a subset (or unary relation) of Env:
〈b〉 = {η : [[b]]η = true}
This can be extended to a binary relation (i.e. a program):
[[b]] = {(η, η) : η ∈ 〈b〉}
Intuitively, b corresponds to the program
if b then skip else ⊥ fi
81
Conditional, better attempt
[[if b then P else Q fi]] = [[b;P]] ∪ [[¬b;Q]]
82
While
while b do P od
Do 0 or more executions of P while b holds
Terminate when b does not hold
How to do “0 or more” executions of (b;P)?
83
While
while b do P od
Do 0 or more executions of (b;P)
Terminate with an execution of ¬b
How to do “0 or more” executions of (b;P)?
84
While
while b do P od
Do 0 or more executions of (b;P)
Terminate with an execution of ¬b
How to do “0 or more” executions of (b;P)?
85
Transitive closure
Given a binary relation R ⊆ E × E , the transitive closure of R, R∗
is defined to be the limit of the sequence
R0 ∪ R1 ∪ R2 · · ·
where
R0 = ∆, the diagonal relation
Rn+1 = Rn;R
NB
R∗ is the smallest transitive relation which contains R
Related to the Kleene star operation seen in languages: Σ∗
Technically, R∗ is the least-fixed point of f (X ) = X ∪ X ;R
86
Transitive closure
Given a binary relation R ⊆ E × E , the transitive closure of R, R∗
is defined to be the limit of the sequence
R0 ∪ R1 ∪ R2 · · ·
where
R0 = ∆, the diagonal relation
Rn+1 = Rn;R
NB
R∗ is the smallest transitive relation which contains R
Related to the Kleene star operation seen in languages: Σ∗
Technically, R∗ is the least-fixed point of f (X ) = X ∪ X ;R
87
While
[[while b do P od]] = [[b;P]]∗; [[¬b]]
Do 0 or more executions of (b;P)
Conclude with an execution of ¬b
88
Validity
A Hoare triple is valid, written |= {ϕ}P {ψ} if
[[P]](〈ϕ〉) ⊆ 〈ψ〉.
That is, the relational image under [[P]] of the set of states where
ϕ holds is contained in the set of states where ψ holds.
89
Validity
90
Validity
〈ϕ〉
91
Validity
〈ϕ〉 〈ψ〉
92
Validity
〈ϕ〉 〈ψ〉
[[P]]
93
Validity
〈ϕ〉 〈ψ〉[[P]](〈ϕ〉)
[[P]]
94
Soundness of Hoare Logic
Hoare Logic is sound with respect to the semantics given. That is,
Theorem
If ` {ϕ}P {ψ} then |= {ϕ}P {ψ}
95
Summary
Set theory revisited
Soundness of Hoare Logic
Completeness of Hoare Logic
96
Summary
Set theory revisited
Soundness of Hoare Logic
Completeness of Hoare Logic
97
Some results on relational images
Lemma
For any binary relations R, S ⊆ X × Y and subsets A,B ⊆ X :
(a) If A ⊆ B then R(A) ⊆ R(B)
(b) R(A) ∪ S(A) = (R ∪ S)(A)
(c) R(S(A)) = (S ;R)(A)
Proof (a):
98
Some results on relational images
Lemma
For any binary relations R, S ⊆ X × Y and subsets A,B ⊆ X :
(a) If A ⊆ B then R(A) ⊆ R(B)
(b) R(A) ∪ S(A) = (R ∪ S)(A)
(c) R(S(A)) = (S ;R)(A)
Proof (a):
99
Some results on relational images
Lemma
For any binary relations R, S ⊆ X × Y and subsets A,B ⊆ X :
(a) If A ⊆ B then R(A) ⊆ R(B)
(b) R(A) ∪ S(A) = (R ∪ S)(A)
(c) R(S(A)) = (S ;R)(A)
Proof (a):
y ∈ R(A) ⇔ ∃x ∈ A such that (x , y) ∈ R
⇒ ∃x ∈ B such that (x , y) ∈ R
⇔ y ∈ R(B)
100
Some results on relational images
Lemma
For any binary relations R, S ⊆ X × Y and subsets A,B ⊆ X :
(a) If A ⊆ B then R(A) ⊆ R(B)
(b) R(A) ∪ S(A) = (R ∪ S)(A)
(c) R(S(A)) = (S ;R)(A)
Proof (b):
101
Some results on relational images
Lemma
For any binary relations R, S ⊆ X × Y and subsets A,B ⊆ X :
(a) If A ⊆ B then R(A) ⊆ R(B)
(b) R(A) ∪ S(A) = (R ∪ S)(A)
(c) R(S(A)) = (S ;R)(A)
Proof (b):
y ∈ R(A) ∪ S(A) ⇔ y ∈ R(A) or y ∈ S(A)
⇔ ∃x ∈ A s.t. (x , y) ∈ R or ∃x ∈ A s.t. (x , y) ∈ S
⇔ ∃x ∈ A s.t. (x , y) ∈ R or (x , y) ∈ S
⇔ ∃x ∈ A s.t. (x , y) ∈ (R ∪ S)
⇔ y ∈ (R ∪ S)(A)
102
Some results on relational images
Lemma
For any binary relations R, S ⊆ X × Y and subsets A,B ⊆ X :
(a) If A ⊆ B then R(A) ⊆ R(B)
(b) R(A) ∪ S(A) = (R ∪ S)(A)
(c) R(S(A)) = (S ;R)(A)
Proof (c):
103
Some results on relational images
Lemma
For any binary relations R, S ⊆ X × Y and subsets A,B ⊆ X :
(a) If A ⊆ B then R(A) ⊆ R(B)
(b) R(A) ∪ S(A) = (R ∪ S)(A)
(c) R(S(A)) = (S ;R)(A)
Proof (c):
z ∈ R(S(A)) ⇔ ∃y ∈ S(A) s.t. (y , z) ∈ R
⇔ ∃x ∈ A, y ∈ S(A) s.t. (x , y) ∈ S and (y , z) ∈ R
⇔ ∃x ∈ A s.t. (x , z) ∈ (S ;R)
⇔ z ∈ (S ;R)(A)
104
Some results on relational images
Corollary
If R(A) ⊆ A then R∗(A) ⊆ A
Proof:
R(A) ⊆ A ⇒ R i+1(A) = R i (R(A)) ⊆ R i (A)
⇒ R i+1(A) ⊆ R(A) ⊆ A
So R∗(A) =
( ∞⋃
i=0
R i
)
(A)
=
∞⋃
i=0
R i (A)
⊆ A
105
Some results on relational images
Corollary
If R(A) ⊆ A then R∗(A) ⊆ A
Proof:
R(A) ⊆ A ⇒ R i+1(A) = R i (R(A)) ⊆ R i (A)
⇒ R i+1(A) ⊆ R(A) ⊆ A
So R∗(A) =
( ∞⋃
i=0
R i
)
(A)
=
∞⋃
i=0
R i (A)
⊆ A
106
Some results on relational images
Corollary
If R(A) ⊆ A then R∗(A) ⊆ A
Proof:
R(A) ⊆ A ⇒ R i+1(A) = R i (R(A)) ⊆ R i (A)
⇒ R i+1(A) ⊆ R(A) ⊆ A
So R∗(A) =
( ∞⋃
i=0
R i
)
(A)
=
∞⋃
i=0
R i (A)
⊆ A
107
Summary
Set theory revisited
Soundness of Hoare Logic
Completeness of Hoare Logic
108
Soundness of Hoare Logic
Theorem
If ` {ϕ}P {ψ} then |= {ϕ}P {ψ}
Proof:
By induction on the structure of the proof.
109
Soundness of Hoare Logic
Theorem
If ` {ϕ}P {ψ} then |= {ϕ}P {ψ}
Proof:
By induction on the structure of the proof.
110
Soundness of Hoare Logic
Theorem
If ` {ϕ}P {ψ} then |= {ϕ}P {ψ}
Proof:
By induction on the structure of the proof.
111
Base case: Assignment rule
(ass){ϕ[e/x ]} x := e {ϕ}
Need to show {ϕ[e/x ]} x := e {ϕ} is always valid. That is,
[[x := e]](〈ϕ[e/x ]〉) ⊆ 〈ϕ〉.
Observation: [[ϕ[e/x ]]]η = [[ϕ]]η
′
where η′ = η[x 7→ [[e]]η]
So if η ∈ 〈ϕ[e/x ]〉 then η′ ∈ 〈ϕ〉
Recall: (η, η′′) ∈ [[x := e]] if and only if η′′ = η[x 7→ [[e]]η],
So [[x := e]](η) ∈ 〈ϕ〉 for all η ∈ 〈ϕ[e/x ]〉
So [[x := e]](〈ϕ[e/x ]〉) ⊆ 〈ϕ〉
112
Base case: Assignment rule
(ass){ϕ[e/x ]} x := e {ϕ}
Need to show {ϕ[e/x ]} x := e {ϕ} is always valid. That is,
[[x := e]](〈ϕ[e/x ]〉) ⊆ 〈ϕ〉.
Observation: [[ϕ[e/x ]]]η = [[ϕ]]η
′
where η′ = η[x 7→ [[e]]η]
So if η ∈ 〈ϕ[e/x ]〉 then η′ ∈ 〈ϕ〉
Recall: (η, η′′) ∈ [[x := e]] if and only if η′′ = η[x 7→ [[e]]η],
So [[x := e]](η) ∈ 〈ϕ〉 for all η ∈ 〈ϕ[e/x ]〉
So [[x := e]](〈ϕ[e/x ]〉) ⊆ 〈ϕ〉
113
Base case: Assignment rule
(ass){ϕ[e/x ]} x := e {ϕ}
Need to show {ϕ[e/x ]} x := e {ϕ} is always valid. That is,
[[x := e]](〈ϕ[e/x ]〉) ⊆ 〈ϕ〉.
Observation: [[ϕ[e/x ]]]η = [[ϕ]]η
′
where η′ = η[x 7→ [[e]]η]
So if η ∈ 〈ϕ[e/x ]〉 then η′ ∈ 〈ϕ〉
Recall: (η, η′′) ∈ [[x := e]] if and only if η′′ = η[x 7→ [[e]]η],
So [[x := e]](η) ∈ 〈ϕ〉 for all η ∈ 〈ϕ[e/x ]〉
So [[x := e]](〈ϕ[e/x ]〉) ⊆ 〈ϕ〉
114
Base case: Assignment rule
(ass){ϕ[e/x ]} x := e {ϕ}
Need to show {ϕ[e/x ]} x := e {ϕ} is always valid. That is,
[[x := e]](〈ϕ[e/x ]〉) ⊆ 〈ϕ〉.
Observation: [[ϕ[e/x ]]]η = [[ϕ]]η
′
where η′ = η[x 7→ [[e]]η]
So if η ∈ 〈ϕ[e/x ]〉 then η′ ∈ 〈ϕ〉
Recall: (η, η′′) ∈ [[x := e]] if and only if η′′ = η[x 7→ [[e]]η],
So [[x := e]](η) ∈ 〈ϕ〉 for all η ∈ 〈ϕ[e/x ]〉
So [[x := e]](〈ϕ[e/x ]〉) ⊆ 〈ϕ〉
115
Base case: Assignment rule
(ass){ϕ[e/x ]} x := e {ϕ}
Need to show {ϕ[e/x ]} x := e {ϕ} is always valid. That is,
[[x := e]](〈ϕ[e/x ]〉) ⊆ 〈ϕ〉.
Observation: [[ϕ[e/x ]]]η = [[ϕ]]η
′
where η′ = η[x 7→ [[e]]η]
So if η ∈ 〈ϕ[e/x ]〉 then η′ ∈ 〈ϕ〉
Recall: (η, η′′) ∈ [[x := e]] if and only if η′′ = η[x 7→ [[e]]η],
So [[x := e]](η) ∈ 〈ϕ〉 for all η ∈ 〈ϕ[e/x ]〉
So [[x := e]](〈ϕ[e/x ]〉) ⊆ 〈ϕ〉
116
Base case: Assignment rule
(ass){ϕ[e/x ]} x := e {ϕ}
Need to show {ϕ[e/x ]} x := e {ϕ} is always valid. That is,
[[x := e]](〈ϕ[e/x ]〉) ⊆ 〈ϕ〉.
Observation: [[ϕ[e/x ]]]η = [[ϕ]]η
′
where η′ = η[x 7→ [[e]]η]
So if η ∈ 〈ϕ[e/x ]〉 then η′ ∈ 〈ϕ〉
Recall: (η, η′′) ∈ [[x := e]] if and only if η′′ = η[x 7→ [[e]]η],
So [[x := e]](η) ∈ 〈ϕ〉 for all η ∈ 〈ϕ[e/x ]〉
So [[x := e]](〈ϕ[e/x ]〉) ⊆ 〈ϕ〉
117
Base case: Assignment rule
(ass){ϕ[e/x ]} x := e {ϕ}
Need to show {ϕ[e/x ]} x := e {ϕ} is always valid. That is,
[[x := e]](〈ϕ[e/x ]〉) ⊆ 〈ϕ〉.
Observation: [[ϕ[e/x ]]]η = [[ϕ]]η
′
where η′ = η[x 7→ [[e]]η]
So if η ∈ 〈ϕ[e/x ]〉 then η′ ∈ 〈ϕ〉
Recall: (η, η′′) ∈ [[x := e]] if and only if η′′ = η[x 7→ [[e]]η],
So [[x := e]](η) ∈ 〈ϕ〉 for all η ∈ 〈ϕ[e/x ]〉
So [[x := e]](〈ϕ[e/x ]〉) ⊆ 〈ϕ〉
118
Inductive case 1: Sequence rule
{ϕ}P {ψ} {ψ}Q {ρ}
(seq){ϕ}P;Q {ρ}
Assume {ϕ}P {ψ} and {ψ}Q {ρ} are valid. Need to show that
{ϕ}P;Q {ρ} is valid.
Recall: [[P;Q]] = [[P]]; [[Q]]
So: [[P;Q]](〈ϕ〉) = [[Q]]([[P]](〈ϕ〉)) (see Lemma 1(c))
By IH: [[P]](〈ϕ〉) ⊆ 〈ψ〉 and [[Q]](〈ψ〉) ⊆ 〈ρ〉
So: [[Q]]
(
[[P]](〈ϕ〉)) ⊆ [[Q]](〈ψ〉) ⊆ 〈ρ〉 (see Lemma 1(a))
119
Inductive case 1: Sequence rule
{ϕ}P {ψ} {ψ}Q {ρ}
(seq){ϕ}P;Q {ρ}
Assume {ϕ}P {ψ} and {ψ}Q {ρ} are valid. Need to show that
{ϕ}P;Q {ρ} is valid.
Recall: [[P;Q]] = [[P]]; [[Q]]
So: [[P;Q]](〈ϕ〉) = [[Q]]([[P]](〈ϕ〉)) (see Lemma 1(c))
By IH: [[P]](〈ϕ〉) ⊆ 〈ψ〉 and [[Q]](〈ψ〉) ⊆ 〈ρ〉
So: [[Q]]
(
[[P]](〈ϕ〉)) ⊆ [[Q]](〈ψ〉) ⊆ 〈ρ〉 (see Lemma 1(a))
120
Inductive case 1: Sequence rule
{ϕ}P {ψ} {ψ}Q {ρ}
(seq){ϕ}P;Q {ρ}
Assume {ϕ}P {ψ} and {ψ}Q {ρ} are valid. Need to show that
{ϕ}P;Q {ρ} is valid.
Recall: [[P;Q]] = [[P]]; [[Q]]
So: [[P;Q]](〈ϕ〉) = [[Q]]([[P]](〈ϕ〉)) (see Lemma 1(c))
By IH: [[P]](〈ϕ〉) ⊆ 〈ψ〉 and [[Q]](〈ψ〉) ⊆ 〈ρ〉
So: [[Q]]
(
[[P]](〈ϕ〉)) ⊆ [[Q]](〈ψ〉) ⊆ 〈ρ〉 (see Lemma 1(a))
121
Inductive case 1: Sequence rule
{ϕ}P {ψ} {ψ}Q {ρ}
(seq){ϕ}P;Q {ρ}
Assume {ϕ}P {ψ} and {ψ}Q {ρ} are valid. Need to show that
{ϕ}P;Q {ρ} is valid.
Recall: [[P;Q]] = [[P]]; [[Q]]
So: [[P;Q]](〈ϕ〉) = [[Q]]([[P]](〈ϕ〉)) (see Lemma 1(c))
By IH: [[P]](〈ϕ〉) ⊆ 〈ψ〉 and [[Q]](〈ψ〉) ⊆ 〈ρ〉
So: [[Q]]
(
[[P]](〈ϕ〉)) ⊆ [[Q]](〈ψ〉) ⊆ 〈ρ〉 (see Lemma 1(a))
122
Inductive case 1: Sequence rule
{ϕ}P {ψ} {ψ}Q {ρ}
(seq){ϕ}P;Q {ρ}
Assume {ϕ}P {ψ} and {ψ}Q {ρ} are valid. Need to show that
{ϕ}P;Q {ρ} is valid.
Recall: [[P;Q]] = [[P]]; [[Q]]
So: [[P;Q]](〈ϕ〉) = [[Q]]([[P]](〈ϕ〉)) (see Lemma 1(c))
By IH: [[P]](〈ϕ〉) ⊆ 〈ψ〉 and [[Q]](〈ψ〉) ⊆ 〈ρ〉
So: [[Q]]
(
[[P]](〈ϕ〉)) ⊆ [[Q]](〈ψ〉) ⊆ 〈ρ〉 (see Lemma 1(a))
123
Inductive case 1: Sequence rule
{ϕ}P {ψ} {ψ}Q {ρ}
(seq){ϕ}P;Q {ρ}
Assume {ϕ}P {ψ} and {ψ}Q {ρ} are valid. Need to show that
{ϕ}P;Q {ρ} is valid.
Recall: [[P;Q]] = [[P]]; [[Q]]
So: [[P;Q]](〈ϕ〉) = [[Q]]([[P]](〈ϕ〉)) (see Lemma 1(c))
By IH: [[P]](〈ϕ〉) ⊆ 〈ψ〉 and [[Q]](〈ψ〉) ⊆ 〈ρ〉
So: [[Q]]
(
[[P]](〈ϕ〉)) ⊆ [[Q]](〈ψ〉) ⊆ 〈ρ〉 (see Lemma 1(a))
124
Two more useful results
Lemma
For R ⊆ Env×Env, predicates ϕ and ψ, and X ⊆ Env:
(a) [[ϕ]](X ) = 〈ϕ〉 ∩ X
(b) R(〈ϕ ∧ ψ〉) = ([[ϕ]];R)(〈ψ〉))
Proof (a):
125
Two more useful results
Lemma
For R ⊆ Env×Env, predicates ϕ and ψ, and X ⊆ Env:
(a) [[ϕ]](X ) = 〈ϕ〉 ∩ X
(b) R(〈ϕ ∧ ψ〉) = ([[ϕ]];R)(〈ψ〉))
Proof (a):
126
Two more useful results
Lemma
For R ⊆ Env×Env, predicates ϕ and ψ, and X ⊆ Env:
(a) [[ϕ]](X ) = 〈ϕ〉 ∩ X
(b) R(〈ϕ ∧ ψ〉) = ([[ϕ]];R)(〈ψ〉))
Proof (a):
η′ ∈ [[ϕ]](X ) ⇔ ∃η ∈ X s.t. (η, η′) ∈ [[ϕ]]
⇔ ∃η ∈ X s.t. η = η′ and η ∈ 〈ϕ〉
⇔ η′ ∈ X ∩ 〈ϕ〉
127
Two more useful results
Lemma
For R ⊆ Env×Env, predicates ϕ and ψ, and X ⊆ Env:
(a) [[ϕ]](X ) = 〈ϕ〉 ∩ X
(b) R(〈ϕ ∧ ψ〉) = ([[ϕ]];R)(〈ψ〉))
Proof (b):
〈ϕ ∧ ψ〉 = 〈ϕ〉 ∩ 〈ψ〉 = [[ϕ]](〈ψ〉)
So R(〈ϕ ∧ ψ〉) = R([[ϕ]](〈ψ〉))
= ([[ϕ]];R)(〈ψ〉) (see Lemma 1(b))
128
Inductive case 2: Conditional rule
{ϕ ∧ g}P {ψ} {ϕ ∧ ¬g}Q {ψ}
(if){ϕ} if g then P else Q fi {ψ}
Assume {ϕ ∧ g}P {ψ} and {ϕ ∧ ¬g}Q {ψ} are valid. Need to
show that {ϕ} if g then P else Q fi {ψ} is valid.
Recall: [[if g then P else Q fi]] = [[g ;P]] ∪ [[¬g ;Q]]
[[if g then P else Q fi]](〈ϕ〉)
= [[g ;P]](〈ϕ〉) ∪ [[¬g ;Q]](〈ϕ〉) (see Lemma 1(b))
= [[P]](〈g ∧ ϕ〉) ∪ [[Q]](〈¬g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ψ〉 (by IH)
129
Inductive case 2: Conditional rule
{ϕ ∧ g}P {ψ} {ϕ ∧ ¬g}Q {ψ}
(if){ϕ} if g then P else Q fi {ψ}
Assume {ϕ ∧ g}P {ψ} and {ϕ ∧ ¬g}Q {ψ} are valid. Need to
show that {ϕ} if g then P else Q fi {ψ} is valid.
Recall: [[if g then P else Q fi]] = [[g ;P]] ∪ [[¬g ;Q]]
[[if g then P else Q fi]](〈ϕ〉)
= [[g ;P]](〈ϕ〉) ∪ [[¬g ;Q]](〈ϕ〉) (see Lemma 1(b))
= [[P]](〈g ∧ ϕ〉) ∪ [[Q]](〈¬g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ψ〉 (by IH)
130
Inductive case 2: Conditional rule
{ϕ ∧ g}P {ψ} {ϕ ∧ ¬g}Q {ψ}
(if){ϕ} if g then P else Q fi {ψ}
Assume {ϕ ∧ g}P {ψ} and {ϕ ∧ ¬g}Q {ψ} are valid. Need to
show that {ϕ} if g then P else Q fi {ψ} is valid.
Recall: [[if g then P else Q fi]] = [[g ;P]] ∪ [[¬g ;Q]]
[[if g then P else Q fi]](〈ϕ〉)
= [[g ;P]](〈ϕ〉) ∪ [[¬g ;Q]](〈ϕ〉) (see Lemma 1(b))
= [[P]](〈g ∧ ϕ〉) ∪ [[Q]](〈¬g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ψ〉 (by IH)
131
Inductive case 2: Conditional rule
{ϕ ∧ g}P {ψ} {ϕ ∧ ¬g}Q {ψ}
(if){ϕ} if g then P else Q fi {ψ}
Assume {ϕ ∧ g}P {ψ} and {ϕ ∧ ¬g}Q {ψ} are valid. Need to
show that {ϕ} if g then P else Q fi {ψ} is valid.
Recall: [[if g then P else Q fi]] = [[g ;P]] ∪ [[¬g ;Q]]
[[if g then P else Q fi]](〈ϕ〉)
= [[g ;P]](〈ϕ〉) ∪ [[¬g ;Q]](〈ϕ〉) (see Lemma 1(b))
= [[P]](〈g ∧ ϕ〉) ∪ [[Q]](〈¬g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ψ〉 (by IH)
132
Inductive case 2: Conditional rule
{ϕ ∧ g}P {ψ} {ϕ ∧ ¬g}Q {ψ}
(if){ϕ} if g then P else Q fi {ψ}
Assume {ϕ ∧ g}P {ψ} and {ϕ ∧ ¬g}Q {ψ} are valid. Need to
show that {ϕ} if g then P else Q fi {ψ} is valid.
Recall: [[if g then P else Q fi]] = [[g ;P]] ∪ [[¬g ;Q]]
[[if g then P else Q fi]](〈ϕ〉)
= [[g ;P]](〈ϕ〉) ∪ [[¬g ;Q]](〈ϕ〉) (see Lemma 1(b))
= [[P]](〈g ∧ ϕ〉) ∪ [[Q]](〈¬g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ψ〉 (by IH)
133
Inductive case 2: Conditional rule
{ϕ ∧ g}P {ψ} {ϕ ∧ ¬g}Q {ψ}
(if){ϕ} if g then P else Q fi {ψ}
Assume {ϕ ∧ g}P {ψ} and {ϕ ∧ ¬g}Q {ψ} are valid. Need to
show that {ϕ} if g then P else Q fi {ψ} is valid.
Recall: [[if g then P else Q fi]] = [[g ;P]] ∪ [[¬g ;Q]]
[[if g then P else Q fi]](〈ϕ〉)
= [[g ;P]](〈ϕ〉) ∪ [[¬g ;Q]](〈ϕ〉) (see Lemma 1(b))
= [[P]](〈g ∧ ϕ〉) ∪ [[Q]](〈¬g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ψ〉 (by IH)
134
Inductive case 2: Conditional rule
{ϕ ∧ g}P {ψ} {ϕ ∧ ¬g}Q {ψ}
(if){ϕ} if g then P else Q fi {ψ}
Assume {ϕ ∧ g}P {ψ} and {ϕ ∧ ¬g}Q {ψ} are valid. Need to
show that {ϕ} if g then P else Q fi {ψ} is valid.
Recall: [[if g then P else Q fi]] = [[g ;P]] ∪ [[¬g ;Q]]
[[if g then P else Q fi]](〈ϕ〉)
= [[g ;P]](〈ϕ〉) ∪ [[¬g ;Q]](〈ϕ〉) (see Lemma 1(b))
= [[P]](〈g ∧ ϕ〉) ∪ [[Q]](〈¬g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ψ〉 (by IH)
135
Inductive case 3: While rule
{ϕ ∧ g}P {ϕ}
(loop){ϕ}while g do P od {ϕ ∧ ¬g}
Assume {ϕ ∧ g}P {ϕ} is valid. Need to show that
{ϕ}while g do P od {ϕ ∧ ¬g}is valid.
Recall: [[while g do P od]] = [[g ;P]]∗; [[¬g ]]
[[g ;P]](〈ϕ〉) = [[P]](〈g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ϕ〉 (IH)
So [[g ;P]]∗(〈ϕ〉) ⊆ 〈ϕ〉 (see Corollary)
So [[g ;P]]∗; [[¬g ]](〈ϕ〉) = [[¬g ]]([[g ;P]]∗(〈ϕ〉)) (see Lemma 1(c))
⊆ [[¬g ]](〈ϕ〉) (see Lemma 1(a))
= 〈¬g ∧ ϕ〉 (see Lemma 2(a))
136
Inductive case 3: While rule
{ϕ ∧ g}P {ϕ}
(loop){ϕ}while g do P od {ϕ ∧ ¬g}
Assume {ϕ ∧ g}P {ϕ} is valid. Need to show that
{ϕ}while g do P od {ϕ ∧ ¬g}is valid.
Recall: [[while g do P od]] = [[g ;P]]∗; [[¬g ]]
[[g ;P]](〈ϕ〉) = [[P]](〈g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ϕ〉 (IH)
So [[g ;P]]∗(〈ϕ〉) ⊆ 〈ϕ〉 (see Corollary)
So [[g ;P]]∗; [[¬g ]](〈ϕ〉) = [[¬g ]]([[g ;P]]∗(〈ϕ〉)) (see Lemma 1(c))
⊆ [[¬g ]](〈ϕ〉) (see Lemma 1(a))
= 〈¬g ∧ ϕ〉 (see Lemma 2(a))
137
Inductive case 3: While rule
{ϕ ∧ g}P {ϕ}
(loop){ϕ}while g do P od {ϕ ∧ ¬g}
Assume {ϕ ∧ g}P {ϕ} is valid. Need to show that
{ϕ}while g do P od {ϕ ∧ ¬g}is valid.
Recall: [[while g do P od]] = [[g ;P]]∗; [[¬g ]]
[[g ;P]](〈ϕ〉) = [[P]](〈g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ϕ〉 (IH)
So [[g ;P]]∗(〈ϕ〉) ⊆ 〈ϕ〉 (see Corollary)
So [[g ;P]]∗; [[¬g ]](〈ϕ〉) = [[¬g ]]([[g ;P]]∗(〈ϕ〉)) (see Lemma 1(c))
⊆ [[¬g ]](〈ϕ〉) (see Lemma 1(a))
= 〈¬g ∧ ϕ〉 (see Lemma 2(a))
138
Inductive case 3: While rule
{ϕ ∧ g}P {ϕ}
(loop){ϕ}while g do P od {ϕ ∧ ¬g}
Assume {ϕ ∧ g}P {ϕ} is valid. Need to show that
{ϕ}while g do P od {ϕ ∧ ¬g}is valid.
Recall: [[while g do P od]] = [[g ;P]]∗; [[¬g ]]
[[g ;P]](〈ϕ〉) = [[P]](〈g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ϕ〉 (IH)
So [[g ;P]]∗(〈ϕ〉) ⊆ 〈ϕ〉 (see Corollary)
So [[g ;P]]∗; [[¬g ]](〈ϕ〉) = [[¬g ]]([[g ;P]]∗(〈ϕ〉)) (see Lemma 1(c))
⊆ [[¬g ]](〈ϕ〉) (see Lemma 1(a))
= 〈¬g ∧ ϕ〉 (see Lemma 2(a))
139
Inductive case 3: While rule
{ϕ ∧ g}P {ϕ}
(loop){ϕ}while g do P od {ϕ ∧ ¬g}
Assume {ϕ ∧ g}P {ϕ} is valid. Need to show that
{ϕ}while g do P od {ϕ ∧ ¬g}is valid.
Recall: [[while g do P od]] = [[g ;P]]∗; [[¬g ]]
[[g ;P]](〈ϕ〉) = [[P]](〈g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ϕ〉 (IH)
So [[g ;P]]∗(〈ϕ〉) ⊆ 〈ϕ〉 (see Corollary)
So [[g ;P]]∗; [[¬g ]](〈ϕ〉) = [[¬g ]]([[g ;P]]∗(〈ϕ〉)) (see Lemma 1(c))
⊆ [[¬g ]](〈ϕ〉) (see Lemma 1(a))
= 〈¬g ∧ ϕ〉 (see Lemma 2(a))
140
Inductive case 3: While rule
{ϕ ∧ g}P {ϕ}
(loop){ϕ}while g do P od {ϕ ∧ ¬g}
Assume {ϕ ∧ g}P {ϕ} is valid. Need to show that
{ϕ}while g do P od {ϕ ∧ ¬g}is valid.
Recall: [[while g do P od]] = [[g ;P]]∗; [[¬g ]]
[[g ;P]](〈ϕ〉) = [[P]](〈g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ϕ〉 (IH)
So [[g ;P]]∗(〈ϕ〉) ⊆ 〈ϕ〉 (see Corollary)
So [[g ;P]]∗; [[¬g ]](〈ϕ〉) = [[¬g ]]([[g ;P]]∗(〈ϕ〉)) (see Lemma 1(c))
⊆ [[¬g ]](〈ϕ〉) (see Lemma 1(a))
= 〈¬g ∧ ϕ〉 (see Lemma 2(a))
141
Inductive case 3: While rule
{ϕ ∧ g}P {ϕ}
(loop){ϕ}while g do P od {ϕ ∧ ¬g}
Assume {ϕ ∧ g}P {ϕ} is valid. Need to show that
{ϕ}while g do P od {ϕ ∧ ¬g}is valid.
Recall: [[while g do P od]] = [[g ;P]]∗; [[¬g ]]
[[g ;P]](〈ϕ〉) = [[P]](〈g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ϕ〉 (IH)
So [[g ;P]]∗(〈ϕ〉) ⊆ 〈ϕ〉 (see Corollary)
So [[g ;P]]∗; [[¬g ]](〈ϕ〉) = [[¬g ]]([[g ;P]]∗(〈ϕ〉)) (see Lemma 1(c))
⊆ [[¬g ]](〈ϕ〉) (see Lemma 1(a))
= 〈¬g ∧ ϕ〉 (see Lemma 2(a))
142
Inductive case 3: While rule
{ϕ ∧ g}P {ϕ}
(loop){ϕ}while g do P od {ϕ ∧ ¬g}
Assume {ϕ ∧ g}P {ϕ} is valid. Need to show that
{ϕ}while g do P od {ϕ ∧ ¬g}is valid.
Recall: [[while g do P od]] = [[g ;P]]∗; [[¬g ]]
[[g ;P]](〈ϕ〉) = [[P]](〈g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ϕ〉 (IH)
So [[g ;P]]∗(〈ϕ〉) ⊆ 〈ϕ〉 (see Corollary)
So [[g ;P]]∗; [[¬g ]](〈ϕ〉) = [[¬g ]]([[g ;P]]∗(〈ϕ〉)) (see Lemma 1(c))
⊆ [[¬g ]](〈ϕ〉) (see Lemma 1(a))
= 〈¬g ∧ ϕ〉 (see Lemma 2(a))
143
Inductive case 3: While rule
{ϕ ∧ g}P {ϕ}
(loop){ϕ}while g do P od {ϕ ∧ ¬g}
Assume {ϕ ∧ g}P {ϕ} is valid. Need to show that
{ϕ}while g do P od {ϕ ∧ ¬g}is valid.
Recall: [[while g do P od]] = [[g ;P]]∗; [[¬g ]]
[[g ;P]](〈ϕ〉) = [[P]](〈g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ϕ〉 (IH)
So [[g ;P]]∗(〈ϕ〉) ⊆ 〈ϕ〉 (see Corollary)
So [[g ;P]]∗; [[¬g ]](〈ϕ〉) = [[¬g ]]([[g ;P]]∗(〈ϕ〉)) (see Lemma 1(c))
⊆ [[¬g ]](〈ϕ〉) (see Lemma 1(a))
= 〈¬g ∧ ϕ〉 (see Lemma 2(a))
144
Inductive case 4: Consequence rule
ϕ′ → ϕ {ϕ}P {ψ} ψ → ψ′
(cons){ϕ′}P {ψ′}
Assume {ϕ}P {ψ} is valid and ϕ′ → ϕ and ψ → ψ′. Need to show
that {ϕ′}P {ψ′} is valid.
Observe: If ϕ′ → ϕ then 〈ϕ′〉 ⊆ 〈ϕ〉
[[P]](〈ϕ′〉) ⊆ [[P]](〈ϕ〉) (see Lemma 1(a))
⊆ 〈ψ〉 (IH)
⊆ 〈ψ′〉
145
Inductive case 4: Consequence rule
ϕ′ → ϕ {ϕ}P {ψ} ψ → ψ′
(cons){ϕ′}P {ψ′}
Assume {ϕ}P {ψ} is valid and ϕ′ → ϕ and ψ → ψ′. Need to show
that {ϕ′}P {ψ′} is valid.
Observe: If ϕ′ → ϕ then 〈ϕ′〉 ⊆ 〈ϕ〉
[[P]](〈ϕ′〉) ⊆ [[P]](〈ϕ〉) (see Lemma 1(a))
⊆ 〈ψ〉 (IH)
⊆ 〈ψ′〉
146
Inductive case 4: Consequence rule
ϕ′ → ϕ {ϕ}P {ψ} ψ → ψ′
(cons){ϕ′}P {ψ′}
Assume {ϕ}P {ψ} is valid and ϕ′ → ϕ and ψ → ψ′. Need to show
that {ϕ′}P {ψ′} is valid.
Observe: If ϕ′ → ϕ then 〈ϕ′〉 ⊆ 〈ϕ〉
[[P]](〈ϕ′〉) ⊆ [[P]](〈ϕ〉) (see Lemma 1(a))
⊆ 〈ψ〉 (IH)
⊆ 〈ψ′〉
147
Inductive case 4: Consequence rule
ϕ′ → ϕ {ϕ}P {ψ} ψ → ψ′
(cons){ϕ′}P {ψ′}
Assume {ϕ}P {ψ} is valid and ϕ′ → ϕ and ψ → ψ′. Need to show
that {ϕ′}P {ψ′} is valid.
Observe: If ϕ′ → ϕ then 〈ϕ′〉 ⊆ 〈ϕ〉
[[P]](〈ϕ′〉) ⊆ [[P]](〈ϕ〉) (see Lemma 1(a))
⊆ 〈ψ〉 (IH)
⊆ 〈ψ′〉
148
Inductive case 4: Consequence rule
ϕ′ → ϕ {ϕ}P {ψ} ψ → ψ′
(cons){ϕ′}P {ψ′}
Assume {ϕ}P {ψ} is valid and ϕ′ → ϕ and ψ → ψ′. Need to show
that {ϕ′}P {ψ′} is valid.
Observe: If ϕ′ → ϕ then 〈ϕ′〉 ⊆ 〈ϕ〉
[[P]](〈ϕ′〉) ⊆ [[P]](〈ϕ〉) (see Lemma 1(a))
⊆ 〈ψ〉 (IH)
⊆ 〈ψ′〉
149
Soundness of Hoare Logic
Theorem
If ` {ϕ}P {ψ} then |= {ϕ}P {ψ}
150
Summary
Set theory revisited
Soundness of Hoare Logic
Completeness of Hoare Logic
151
Incompleteness
Theorem (Go¨del’s Incompleteness Theorem)
There is no proof system that can prove every valid first-order
sentence about arithmetic over the natural numbers.
⇒ There are true statements that do not have a proof.
⇒ Because of (cons) there are valid triples that result from valid,
but unprovable, consequences.
⇒ Hoare Logic is not complete.
152
Incompleteness
Theorem (Go¨del’s Incompleteness Theorem)
There is no proof system that can prove every valid first-order
sentence about arithmetic over the natural numbers.
⇒ There are true statements that do not have a proof.
⇒ Because of (cons) there are valid triples that result from valid,
but unprovable, consequences.
⇒ Hoare Logic is not complete.
153
Incompleteness
Theorem (Go¨del’s Incompleteness Theorem)
There is no proof system that can prove every valid first-order
sentence about arithmetic over the natural numbers.
⇒ There are true statements that do not have a proof.
⇒ Because of (cons) there are valid triples that result from valid,
but unprovable, consequences.
⇒ Hoare Logic is not complete.
154
Incompleteness
Theorem (Go¨del’s Incompleteness Theorem)
There is no proof system that can prove every valid first-order
sentence about arithmetic over the natural numbers.
⇒ There are true statements that do not have a proof.
⇒ Because of (cons) there are valid triples that result from valid,
but unprovable, consequences.
⇒ Hoare Logic is not complete.
155
Relative completeness of Hoare Logic
Theorem (Relative completeness of Hoare Logic)
With an oracle that decides the validity of predicates,
if |= {ϕ}P {ψ} then ` {ϕ}P {ψ} .
156
Need to know for this course
Write programs in L.
Give proofs using the Hoare logic rules (full and outline)
Definition of [[·]]
Definition of composition and transitive closure
Term 1, 2023
Hoare Logic
1
Sir Tony Hoare
Pioneer in formal verification
Invented: Quicksort,
the null reference (called it his “billion dollar mistake”)
CSP (formal specification language), and
Hoare Logic
2
Summary
L: A simple imperative programming language
Hoare triples (SYNTAX)
Hoare logic (PROOF)
Semantics for Hoare logic
3
Summary
L: A simple imperative programming language
Hoare triples (SYNTAX)
Hoare logic (PROOF)
Semantics for Hoare logic
4
Imperative Programming
impero¯
Definition
Imperative programming is where programs are described as a
series of statements or commands to manipulate mutable state or
cause externally observable effects.
States may take the form of a mapping from variable names to
their values, or even a model of a CPU state with a memory model
(for example, in an assembly language).
5
L: A simple imperative programming language
Consider the vocabulary of basic arithmetic:
Constant symbols: 0, 1, 2, . . .
Function symbols: +, ∗, . . .
Predicate symbols: <,≤,≥, |, . . .
An (arithmetic) expression is a term over this vocabulary.
A boolean expression is a predicate formula over this
vocabulary.
6
L: A simple imperative programming language
Consider the vocabulary of basic arithmetic:
Constant symbols: 0, 1, 2, . . .
Function symbols: +, ∗, . . .
Predicate symbols: <,≤,≥, |, . . .
An (arithmetic) expression is a term over this vocabulary.
A boolean expression is a predicate formula over this
vocabulary.
7
L: A simple imperative programming language
Consider the vocabulary of basic arithmetic:
Constant symbols: 0, 1, 2, . . .
Function symbols: +, ∗, . . .
Predicate symbols: <,≤,≥, |, . . .
An (arithmetic) expression is a term over this vocabulary.
A boolean expression is a predicate formula over this
vocabulary.
8
The language L
The language L is a simple imperative programming language
made up of four statements:
Assignment: x :=e
where x is a variable and e is an arithmetic
expression.
Sequencing: P;Q
Conditional: if g then P else Q fi
where g is a boolean expression.
While: while g do P od
9
The language L
The language L is a simple imperative programming language
made up of four statements:
Assignment: x :=e
where x is a variable and e is an arithmetic
expression.
Sequencing: P;Q
Conditional: if g then P else Q fi
where g is a boolean expression.
While: while g do P od
10
The language L
The language L is a simple imperative programming language
made up of four statements:
Assignment: x :=e
where x is a variable and e is an arithmetic
expression.
Sequencing: P;Q
Conditional: if g then P else Q fi
where g is a boolean expression.
While: while g do P od
11
The language L
The language L is a simple imperative programming language
made up of four statements:
Assignment: x :=e
where x is a variable and e is an arithmetic
expression.
Sequencing: P;Q
Conditional: if g then P else Q fi
where g is a boolean expression.
While: while g do P od
12
Factorial in L
Example
i := 0;
m := 1;
while i < N do
i := i + 1;
m := m ∗ i
od
13
Summary
L: A simple imperative programming language
Hoare triples (SYNTAX)
Hoare logic (PROOF)
Semantics for Hoare logic
14
Summary
L: A simple imperative programming language
Hoare triples (SYNTAX)
Hoare logic (PROOF)
Semantics for Hoare logic
15
Hoare Logic
We are going to define what’s called a Hoare Logic for L to allow
us to prove properties of our program.
We write a Hoare triple judgement as:
{ϕ} P {ψ}
Where ϕ and ψ are logical formulae about states, called assertions,
and P is a program. This triple states that if the program P
terminates and it successfully evaluates from a starting state
satisfying the precondition ϕ, then the result state will satisfy the
postcondition ψ.
16
Hoare triple: Examples
Example
{(x = 0)} x := 1 {(x = 1)}
{(x = 499)} x := x + 1 {(x = 500)}
{(x > 0)} y := 0− x {(y < 0) ∧ (x 6= y)}
17
Hoare triple: Examples
Example
{(x = 0)} x := 1 {(x = 1)}
{(x = 499)} x := x + 1 {(x = 500)}
{(x > 0)} y := 0− x {(y < 0) ∧ (x 6= y)}
18
Hoare triple: Examples
Example
{(x = 0)} x := 1 {(x = 1)}
{(x = 499)} x := x + 1 {(x = 500)}
{(x > 0)} y := 0− x {(y < 0) ∧ (x 6= y)}
19
Hoare triple: Factorial Examples
Example
{N ≥ 0}
i := 0;
m := 1;
while i < N do
i := i + 1;
m := m ∗ i
od
{m = N!}
20
Summary
L: A simple imperative programming language
Hoare triples (SYNTAX)
Hoare logic (PROOF)
Semantics for Hoare logic
21
Motivation
Question
We know what we want informally; how do we establish when a
triple is valid?
Develop a semantics, OR
Derive the triple in a syntactic manner (i.e. Hoare proof)
Hoare logic consists of one axiom and four inference rules for
deriving Hoare triples.
22
Motivation
Question
We know what we want informally; how do we establish when a
triple is valid?
Develop a semantics, OR
Derive the triple in a syntactic manner (i.e. Hoare proof)
Hoare logic consists of one axiom and four inference rules for
deriving Hoare triples.
23
Motivation
Question
We know what we want informally; how do we establish when a
triple is valid?
Develop a semantics, OR
Derive the triple in a syntactic manner (i.e. Hoare proof)
Hoare logic consists of one axiom and four inference rules for
deriving Hoare triples.
24
Assignment
(assign){ϕ[e/x ]} x := e {ϕ}
Intuition:
If x has property ϕ after executing the assignment; then e must
have property ϕ before executing the assignment
25
Assignment: Example
Example
{(y = 0)} x := y {(x = 0)}
{
(y = y)
} x := y {(x = y)}
{
(1 < 2)
} x := 1 {(x < 2)}
{(y = 3)} x := y {(x > 2)}
Problem!
26
Assignment: Example
Example
{(y = 0)} x := y {(x = 0)}
{
(y = y)
} x := y {(x = y)}
{
(1 < 2)
} x := 1 {(x < 2)}
{(y = 3)} x := y {(x > 2)}
Problem!
27
Assignment: Example
Example
{(y = 0)} x := y {(x = 0)}
{(y = y)} x := y {(x = y)}
{
(1 < 2)
} x := 1 {(x < 2)}
{(y = 3)} x := y {(x > 2)}
Problem!
28
Assignment: Example
Example
{(y = 0)} x := y {(x = 0)}
{(y = y)} x := y {(x = y)}
{
(1 < 2)
} x := 1 {(x < 2)}
{(y = 3)} x := y {(x > 2)}
Problem!
29
Assignment: Example
Example
{(y = 0)} x := y {(x = 0)}
{(y = y)} x := y {(x = y)}
{(1 < 2)} x := 1 {(x < 2)}
{(y = 3)} x := y {(x > 2)}
Problem!
30
Assignment: Example
Example
{(y = 0)} x := y {(x = 0)}
{(y = y)} x := y {(x = y)}
{(1 < 2)} x := 1 {(x < 2)}
{(y = 3)} x := y {(x > 2)} Problem!
31
Sequence
{ϕ}P {ψ} {ψ}Q {ρ}
(seq){ϕ}P;Q {ρ}
Intuition:
If the postcondition of P matches the precondition of Q we can
sequentially combine the two program fragments
32
Sequence: Example
Example
{
(0 = 0)
} x := 0 {
(x = 0)
} {
(x = 0)
} y := 0 {(x = y)}
(seq){
(0 = 0)
} x := 0; y := 0 {(x = y)}
33
Sequence: Example
Example
{
(0 = 0)
} x := 0 {(x = 0)} {(x = 0)} y := 0 {(x = y)}
(seq){
(0 = 0)
} x := 0; y := 0 {(x = y)}
34
Sequence: Example
Example
{(0 = 0)} x := 0 {(x = 0)} {(x = 0)} y := 0 {(x = y)}
(seq){(0 = 0)} x := 0; y := 0 {(x = y)}
35
Conditional
{ϕ ∧ g}P {ψ} {ϕ ∧ ¬g}Q {ψ}
(if){ϕ} if g then P else Q fi {ψ}
Intuition:
When a conditional is executed, either P or Q will be
executed.
If ψ is a postcondition of the conditional, then it must be a
postcondition of both branches
Likewise, if ϕ is a precondition of the conditional, then it must
be a precondition of both branches
Which branch gets executed depends on g , so we can assume
g to be a precondition of P and ¬g to be a precondition of Q.
36
While
{ϕ ∧ g}P {ϕ}
(loop){ϕ}while g do P od {ϕ ∧ ¬g}
Intuition:
ϕ is a loop invariant. It must be both a pre- and
postcondition of P, so that sequences of Ps can be run
together.
If the while loop terminates, g cannot hold.
37
Consequence
There is one more rule, called the rule of consequence, that we
need to insert ordinary logical reasoning into our Hoare logic
proofs:
ϕ′ → ϕ {ϕ}P {ψ} ψ → ψ′
(cons){ϕ′}P {ψ′}
Intuition:
Adding assertions to the precondition makes it more likely the
postcondition will be reached
Removing assertions from the postcondition makes it more
likely the postcondition will be reached
If you can reach the postcondition initially, then you can reach
it in the more likely scenario
38
Consequence
There is one more rule, called the rule of consequence, that we
need to insert ordinary logical reasoning into our Hoare logic
proofs:
ϕ′ → ϕ {ϕ}P {ψ} ψ → ψ′
(cons){ϕ′}P {ψ′}
Intuition:
Adding assertions to the precondition makes it more likely the
postcondition will be reached
Removing assertions from the postcondition makes it more
likely the postcondition will be reached
If you can reach the postcondition initially, then you can reach
it in the more likely scenario
39
Back to Assignment Example
Example
{(y = 3)} x := y {(x > 2)} Problem!
{(y = 3)}x := y{(x > 2)}(assign, cons)
{(y > 2)}x := y{(x > 2)}(assign)
40
Back to Assignment Example
Example
{(y = 3)} x := y {(x > 2)} Problem!
{(y = 3)}x := y{(x > 2)}(assign, cons)
{(y > 2)}x := y{(x > 2)}(assign)
41
Back to Assignment Example
Example
{(y = 3)} x := y {(x > 2)} Problem!
{(y = 3)}x := y{(x > 2)}(assign, cons)
{(y > 2)}x := y{(x > 2)}(assign)
42
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{N ≥ 0}
{1 = 0! ∧ N ≥ 0}
i := 0;
{1 = i ! ∧ N ≥ 0}
{1 = i ! ∧ N ≥ 0}
m := 1;
{m = i ! ∧ N ≥ 0}
{m = i ! ∧ N ≥ 0}
while i < N do
{m = i ! ∧ N ≥ 0 ∧ i < N}
{m × (i + 1) = (i + 1)! ∧ N ≥ 0}
i := i + 1;
{m × i = i ! ∧ N ≥ 0}
m := m × i
{m = i ! ∧ N ≥ 0}
od
{m = i ! ∧ N ≥ 0 ∧ i = N}
{m = N!}
{ϕ ∧ g} P {ψ} {ϕ ∧ ¬g} Q {ψ}
{ϕ} if g then P else Q fi {ψ}
{ϕ[x := e]} x := e {ϕ}
{ϕ ∧ g} P {ϕ}
{ϕ} while g do P od {ϕ ∧ ¬g}
{ϕ} P {α} {α} Q {ψ}
{ϕ} P;Q {ψ}
ϕ′ ⇒ ϕ {ϕ} P {ψ} ψ ⇒ ψ′
{ϕ′} P {ψ′}
note: (i + 1)! = i!× (i + 1)
43
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{N ≥ 0}
{1 = 0! ∧ N ≥ 0}
i := 0;
{1 = i ! ∧ N ≥ 0}
{1 = i ! ∧ N ≥ 0}
m := 1;
{m = i ! ∧ N ≥ 0}
{m = i ! ∧ N ≥ 0}
while i < N do
{m = i ! ∧ N ≥ 0 ∧ i < N}
{m × (i + 1) = (i + 1)! ∧ N ≥ 0}
i := i + 1;
{m × i = i ! ∧ N ≥ 0}
m := m × i
{m = i ! ∧ N ≥ 0}
od {m = i ! ∧ N ≥ 0 ∧ i = N}
{m = N!}
{ϕ ∧ g} P {ψ} {ϕ ∧ ¬g} Q {ψ}
{ϕ} if g then P else Q fi {ψ}
{ϕ[x := e]} x := e {ϕ}
{ϕ ∧ g} P {ϕ}
{ϕ} while g do P od {ϕ ∧ ¬g}
{ϕ} P {α} {α} Q {ψ}
{ϕ} P;Q {ψ}
ϕ′ ⇒ ϕ {ϕ} P {ψ} ψ ⇒ ψ′
{ϕ′} P {ψ′}
note: (i + 1)! = i!× (i + 1)
44
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{N ≥ 0}
{1 = 0! ∧ N ≥ 0}
i := 0;
{1 = i ! ∧ N ≥ 0}
{1 = i ! ∧ N ≥ 0}
m := 1;
{m = i ! ∧ N ≥ 0}
{m = i ! ∧ N ≥ 0}
while i < N do
{m = i ! ∧ N ≥ 0 ∧ i < N}
{m × (i + 1) = (i + 1)! ∧ N ≥ 0}
i := i + 1;
{m × i = i ! ∧ N ≥ 0}
m := m × i
{m = i ! ∧ N ≥ 0}
od {m = i ! ∧ N ≥ 0 ∧ i = N}
{m = N!}
{ϕ ∧ g} P {ψ} {ϕ ∧ ¬g} Q {ψ}
{ϕ} if g then P else Q fi {ψ}
{ϕ[x := e]} x := e {ϕ}
{ϕ ∧ g} P {ϕ}
{ϕ} while g do P od {ϕ ∧ ¬g}
{ϕ} P {α} {α} Q {ψ}
{ϕ} P;Q {ψ}
ϕ′ ⇒ ϕ {ϕ} P {ψ} ψ ⇒ ψ′
{ϕ′} P {ψ′}
note: (i + 1)! = i!× (i + 1)
45
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{N ≥ 0}
{1 = 0! ∧ N ≥ 0}
i := 0;
{1 = i ! ∧ N ≥ 0}
{1 = i ! ∧ N ≥ 0}
m := 1;
{m = i ! ∧ N ≥ 0}
{m = i ! ∧ N ≥ 0}
while i < N do
{m = i ! ∧ N ≥ 0 ∧ i < N}
{m × (i + 1) = (i + 1)! ∧ N ≥ 0}
i := i + 1;
{m × i = i ! ∧ N ≥ 0}
m := m × i
{m = i ! ∧ N ≥ 0}
od {m = i ! ∧ N ≥ 0 ∧ i = N}
{m = N!}
{ϕ ∧ g} P {ψ} {ϕ ∧ ¬g} Q {ψ}
{ϕ} if g then P else Q fi {ψ}
{ϕ[x := e]} x := e {ϕ}
{ϕ ∧ g} P {ϕ}
{ϕ} while g do P od {ϕ ∧ ¬g}
{ϕ} P {α} {α} Q {ψ}
{ϕ} P;Q {ψ}
ϕ′ ⇒ ϕ {ϕ} P {ψ} ψ ⇒ ψ′
{ϕ′} P {ψ′}
note: (i + 1)! = i!× (i + 1)
46
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{N ≥ 0}
{1 = 0! ∧ N ≥ 0}
i := 0;
{1 = i ! ∧ N ≥ 0}
{1 = i ! ∧ N ≥ 0}
m := 1;
{m = i ! ∧ N ≥ 0}
{m = i ! ∧ N ≥ 0}
while i < N do {m = i ! ∧ N ≥ 0 ∧ i < N}
{m × (i + 1) = (i + 1)! ∧ N ≥ 0}
i := i + 1;
{m × i = i ! ∧ N ≥ 0}
m := m × i
{m = i ! ∧ N ≥ 0}
od {m = i ! ∧ N ≥ 0 ∧ i = N}
{m = N!}
{ϕ ∧ g} P {ψ} {ϕ ∧ ¬g} Q {ψ}
{ϕ} if g then P else Q fi {ψ}
{ϕ[x := e]} x := e {ϕ}
{ϕ ∧ g} P {ϕ}
{ϕ} while g do P od {ϕ ∧ ¬g}
{ϕ} P {α} {α} Q {ψ}
{ϕ} P;Q {ψ}
ϕ′ ⇒ ϕ {ϕ} P {ψ} ψ ⇒ ψ′
{ϕ′} P {ψ′}
note: (i + 1)! = i!× (i + 1)
47
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{N ≥ 0}
{1 = 0! ∧ N ≥ 0}
i := 0;
{1 = i ! ∧ N ≥ 0}
{1 = i ! ∧ N ≥ 0}
m := 1;
{m = i ! ∧ N ≥ 0}
{m = i ! ∧ N ≥ 0}
while i < N do {m = i ! ∧ N ≥ 0 ∧ i < N}
{m × (i + 1) = (i + 1)! ∧ N ≥ 0}
i := i + 1;
{m × i = i ! ∧ N ≥ 0}
m := m × i
{m = i ! ∧ N ≥ 0}
od {m = i ! ∧ N ≥ 0 ∧ i = N}
{m = N!}
{ϕ ∧ g} P {ψ} {ϕ ∧ ¬g} Q {ψ}
{ϕ} if g then P else Q fi {ψ}
{ϕ[x := e]} x := e {ϕ}
{ϕ ∧ g} P {ϕ}
{ϕ} while g do P od {ϕ ∧ ¬g}
{ϕ} P {α} {α} Q {ψ}
{ϕ} P;Q {ψ}
ϕ′ ⇒ ϕ {ϕ} P {ψ} ψ ⇒ ψ′
{ϕ′} P {ψ′}
note: (i + 1)! = i!× (i + 1)
48
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{N ≥ 0}
{1 = 0! ∧ N ≥ 0}
i := 0;
{1 = i ! ∧ N ≥ 0}
{1 = i ! ∧ N ≥ 0}
m := 1;
{m = i ! ∧ N ≥ 0}
{m = i ! ∧ N ≥ 0}
while i < N do {m = i ! ∧ N ≥ 0 ∧ i < N}
{m × (i + 1) = (i + 1)! ∧ N ≥ 0}
i := i + 1;
{m × i = i ! ∧ N ≥ 0}
m := m × i
{m = i ! ∧ N ≥ 0}
od {m = i ! ∧ N ≥ 0 ∧ i = N}
{m = N!}
{ϕ ∧ g} P {ψ} {ϕ ∧ ¬g} Q {ψ}
{ϕ} if g then P else Q fi {ψ}
{ϕ[x := e]} x := e {ϕ}
{ϕ ∧ g} P {ϕ}
{ϕ} while g do P od {ϕ ∧ ¬g}
{ϕ} P {α} {α} Q {ψ}
{ϕ} P;Q {ψ}
ϕ′ ⇒ ϕ {ϕ} P {ψ} ψ ⇒ ψ′
{ϕ′} P {ψ′}
note: (i + 1)! = i!× (i + 1)
49
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{N ≥ 0}
{1 = 0! ∧ N ≥ 0}
i := 0;
{1 = i ! ∧ N ≥ 0}
{1 = i ! ∧ N ≥ 0}
m := 1;
{m = i ! ∧ N ≥ 0}
{m = i ! ∧ N ≥ 0}
while i < N do {m = i ! ∧ N ≥ 0 ∧ i < N}
{m × (i + 1) = (i + 1)! ∧ N ≥ 0}
i := i + 1;
{m × i = i ! ∧ N ≥ 0}
m := m × i
{m = i ! ∧ N ≥ 0}
od {m = i ! ∧ N ≥ 0 ∧ i = N}
{m = N!}
{ϕ ∧ g} P {ψ} {ϕ ∧ ¬g} Q {ψ}
{ϕ} if g then P else Q fi {ψ}
{ϕ[x := e]} x := e {ϕ}
{ϕ ∧ g} P {ϕ}
{ϕ} while g do P od {ϕ ∧ ¬g}
{ϕ} P {α} {α} Q {ψ}
{ϕ} P;Q {ψ}
ϕ′ ⇒ ϕ {ϕ} P {ψ} ψ ⇒ ψ′
{ϕ′} P {ψ′}
note: (i + 1)! = i!× (i + 1)
50
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{N ≥ 0}
{1 = 0! ∧ N ≥ 0}
i := 0;
{1 = i ! ∧ N ≥ 0}
{1 = i ! ∧ N ≥ 0}
m := 1;{m = i ! ∧ N ≥ 0}
{m = i ! ∧ N ≥ 0}
while i < N do {m = i ! ∧ N ≥ 0 ∧ i < N}
{m × (i + 1) = (i + 1)! ∧ N ≥ 0}
i := i + 1;
{m × i = i ! ∧ N ≥ 0}
m := m × i
{m = i ! ∧ N ≥ 0}
od {m = i ! ∧ N ≥ 0 ∧ i = N}
{m = N!}
{ϕ ∧ g} P {ψ} {ϕ ∧ ¬g} Q {ψ}
{ϕ} if g then P else Q fi {ψ}
{ϕ[x := e]} x := e {ϕ}
{ϕ ∧ g} P {ϕ}
{ϕ} while g do P od {ϕ ∧ ¬g}
{ϕ} P {α} {α} Q {ψ}
{ϕ} P;Q {ψ}
ϕ′ ⇒ ϕ {ϕ} P {ψ} ψ ⇒ ψ′
{ϕ′} P {ψ′}
note: (i + 1)! = i!× (i + 1)
51
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{N ≥ 0}
{1 = 0! ∧ N ≥ 0}
i := 0;
{1 = i ! ∧ N ≥ 0}
{1 = i ! ∧ N ≥ 0}m := 1;{m = i ! ∧ N ≥ 0}
{m = i ! ∧ N ≥ 0}
while i < N do {m = i ! ∧ N ≥ 0 ∧ i < N}
{m × (i + 1) = (i + 1)! ∧ N ≥ 0}
i := i + 1;
{m × i = i ! ∧ N ≥ 0}
m := m × i
{m = i ! ∧ N ≥ 0}
od {m = i ! ∧ N ≥ 0 ∧ i = N}
{m = N!}
{ϕ ∧ g} P {ψ} {ϕ ∧ ¬g} Q {ψ}
{ϕ} if g then P else Q fi {ψ}
{ϕ[x := e]} x := e {ϕ}
{ϕ ∧ g} P {ϕ}
{ϕ} while g do P od {ϕ ∧ ¬g}
{ϕ} P {α} {α} Q {ψ}
{ϕ} P;Q {ψ}
ϕ′ ⇒ ϕ {ϕ} P {ψ} ψ ⇒ ψ′
{ϕ′} P {ψ′}
note: (i + 1)! = i!× (i + 1)
52
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{N ≥ 0}
{1 = 0! ∧ N ≥ 0}
i := 0;{1 = i ! ∧ N ≥ 0}
{1 = i ! ∧ N ≥ 0}m := 1;{m = i ! ∧ N ≥ 0}
{m = i ! ∧ N ≥ 0}
while i < N do {m = i ! ∧ N ≥ 0 ∧ i < N}
{m × (i + 1) = (i + 1)! ∧ N ≥ 0}
i := i + 1;
{m × i = i ! ∧ N ≥ 0}
m := m × i
{m = i ! ∧ N ≥ 0}
od {m = i ! ∧ N ≥ 0 ∧ i = N}
{m = N!}
{ϕ ∧ g} P {ψ} {ϕ ∧ ¬g} Q {ψ}
{ϕ} if g then P else Q fi {ψ}
{ϕ[x := e]} x := e {ϕ}
{ϕ ∧ g} P {ϕ}
{ϕ} while g do P od {ϕ ∧ ¬g}
{ϕ} P {α} {α} Q {ψ}
{ϕ} P;Q {ψ}
ϕ′ ⇒ ϕ {ϕ} P {ψ} ψ ⇒ ψ′
{ϕ′} P {ψ′}
note: (i + 1)! = i!× (i + 1)
53
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{N ≥ 0}
{1 = 0! ∧ N ≥ 0} i := 0;{1 = i ! ∧ N ≥ 0}
{1 = i ! ∧ N ≥ 0}m := 1;{m = i ! ∧ N ≥ 0}
{m = i ! ∧ N ≥ 0}
while i < N do {m = i ! ∧ N ≥ 0 ∧ i < N}
{m × (i + 1) = (i + 1)! ∧ N ≥ 0}
i := i + 1;
{m × i = i ! ∧ N ≥ 0}
m := m × i
{m = i ! ∧ N ≥ 0}
od {m = i ! ∧ N ≥ 0 ∧ i = N}
{m = N!}
{ϕ ∧ g} P {ψ} {ϕ ∧ ¬g} Q {ψ}
{ϕ} if g then P else Q fi {ψ}
{ϕ[x := e]} x := e {ϕ}
{ϕ ∧ g} P {ϕ}
{ϕ} while g do P od {ϕ ∧ ¬g}
{ϕ} P {α} {α} Q {ψ}
{ϕ} P;Q {ψ}
ϕ′ ⇒ ϕ {ϕ} P {ψ} ψ ⇒ ψ′
{ϕ′} P {ψ′}
note: (i + 1)! = i!× (i + 1)
54
Practice Exercise
Example
m := 1;
n := 1;
i := 1;
while i < N do
t := m;
m := n;
n := m + t;
i := i + 1
od
What does this L program P compute?
What is a valid Hoare triple {ϕ}P{ψ} of this program?
Prove using the inference rules and consequence axiom that
this Hoare triple is valid.
55
Practice Exercise
Example
m := 1;
n := 1;
i := 1;
while i < N do
t := m;
m := n;
n := m + t;
i := i + 1
od
What does this L program P compute?
What is a valid Hoare triple {ϕ}P{ψ} of this program?
Prove using the inference rules and consequence axiom that
this Hoare triple is valid.
56
Summary
L: A simple imperative programming language
Hoare triples (SYNTAX)
Hoare logic (PROOF)
Semantics for Hoare logic
57
Recall
If R and S are binary relations, then the relational composition
of R and S , R; S is the relation:
R;S := {(a, c) : ∃b such that (a, b) ∈ R and (b, c) ∈ S}
If R ⊆ A× B is a relation, and X ⊆ A, then the image of X
under R, R(X ) is the subset of B defined as:
R(X ) := {b ∈ B : ∃a inX such that (a, b) ∈ R}.
58
Informal semantics
Hoare logic gives a proof of {ϕ}P {ψ}, that is: ` {ϕ}P {ψ}
(axiomatic semantics)
How do we determine when {ϕ}P {ψ} is valid, that is:
|= {ϕ}P {ψ}?
If ϕ holds in a state of some computational model
then ψ holds in the state reached after a successful execution of P.
59
Informal semantics
Hoare logic gives a proof of {ϕ}P {ψ}, that is: ` {ϕ}P {ψ}
(axiomatic semantics)
How do we determine when {ϕ}P {ψ} is valid, that is:
|= {ϕ}P {ψ}?
If ϕ holds in a state of some computational model
then ψ holds in the state reached after a successful execution of P.
60
Informal semantics: Programs
What is a program?
A
partial
function mapping system states to system states
61
Informal semantics: Programs
What is a program?
A
partial
function mapping system states to system states
62
Informal semantics: Programs
What is a program?
A partial function mapping system states to system states
63
Informal semantics: Programs
What is a program?
A relation between system states
64
Informal semantics: States
What is a state of a computational model?
Two approaches:
Concrete: from a physical perspective
States are memory configurations, register contents, etc.
Store of variables and the values associated with them
Abstract: from a mathematical perspective
The pre-/postcondition predicates hold in a state
⇒ States are logical interpretations (Model + Environment)
There is only one model of interest: standard interpretations of
arithmetical symbols
⇒ States are fully determined by environments
⇒ States are functions that map variables to values
65
Informal semantics: States
What is a state of a computational model?
Two approaches:
Concrete: from a physical perspective
States are memory configurations, register contents, etc.
Store of variables and the values associated with them
Abstract: from a mathematical perspective
The pre-/postcondition predicates hold in a state
⇒ States are logical interpretations (Model + Environment)
There is only one model of interest: standard interpretations of
arithmetical symbols
⇒ States are fully determined by environments
⇒ States are functions that map variables to values
66
Informal semantics: States
What is a state of a computational model?
Two approaches:
Concrete: from a physical perspective
States are memory configurations, register contents, etc.
Store of variables and the values associated with them
Abstract: from a mathematical perspective
The pre-/postcondition predicates hold in a state
⇒ States are logical interpretations (Model + Environment)
There is only one model of interest: standard interpretations of
arithmetical symbols
⇒ States are fully determined by environments
⇒ States are functions that map variables to values
67
Informal semantics: States
What is a state of a computational model?
Two approaches:
Concrete: from a physical perspective
States are memory configurations, register contents, etc.
Store of variables and the values associated with them
Abstract: from a mathematical perspective
The pre-/postcondition predicates hold in a state
⇒ States are logical interpretations (Model + Environment)
There is only one model of interest: standard interpretations of
arithmetical symbols
⇒ States are fully determined by environments
⇒ States are functions that map variables to values
68
Informal semantics: States
What is a state of a computational model?
Two approaches:
Concrete: from a physical perspective
States are memory configurations, register contents, etc.
Store of variables and the values associated with them
Abstract: from a mathematical perspective
The pre-/postcondition predicates hold in a state
⇒ States are logical interpretations (Model + Environment)
There is only one model of interest: standard interpretations of
arithmetical symbols
⇒ States are fully determined by environments
⇒ States are functions that map variables to values
69
Informal semantics: States
What is a state of a computational model?
Two approaches:
Concrete: from a physical perspective
States are memory configurations, register contents, etc.
Store of variables and the values associated with them
Abstract: from a mathematical perspective
The pre-/postcondition predicates hold in a state
⇒ States are logical interpretations (Model + Environment)
There is only one model of interest: standard interpretations of
arithmetical symbols
⇒ States are fully determined by environments
⇒ States are functions that map variables to values
70
Informal semantics: States
and Programs
State space (Env)
x ← 1
y ← 1
z ← 2
x ← 0
y ← 0
z ← 0
x ← 0
y ← 1
z ← 2
x ← 3
y ← 2
z ← 1
x ← 0
y ← 1
z ← 0
x ← 1
y ← 1
z ← 1 x ← 2
y ← 2
z ← 2
71
Informal semantics: States and Programs
State space (Env)
x ← 1
y ← 1
z ← 2
x ← 0
y ← 0
z ← 0
x ← 0
y ← 1
z ← 2
x ← 3
y ← 2
z ← 1
x ← 0
y ← 1
z ← 0
x ← 1
y ← 1
z ← 1 x ← 2
y ← 2
z ← 2
72
Informal semantics: States and Programs
73
Semantics for L
An environment or state is a function from variables to numeric
values. We denote by Env the set of all environments.
NB
An environment, η, assigns a numeric value [[e]]η to all expressions
e, and a boolean value [[b]]η to all boolean expressions b.
Given a program P of L, we define [[P]] to be a binary relation on
Env in the following manner...
74
Semantics for L
An environment or state is a function from variables to numeric
values. We denote by Env the set of all environments.
NB
An environment, η, assigns a numeric value [[e]]η to all expressions
e, and a boolean value [[b]]η to all boolean expressions b.
Given a program P of L, we define [[P]] to be a binary relation on
Env in the following manner...
75
Assignment
(η, η′) ∈ [[x := e]] if, and only if η′ = η[x 7→ [[e]]η]
76
Assignment: [[z := 2]]
State space (Env)
x ← 1
y ← 1
z ← 2
x ← 0
y ← 0
z ← 0
x ← 0
y ← 1
z ← 2
x ← 3
y ← 2
z ← 1
x ← 0
y ← 1
z ← 0
x ← 1
y ← 1
z ← 1 x ← 2
y ← 2
z ← 2
77
Sequencing
[[P;Q]] = [[P]]; [[Q]]
where, on the RHS, ; is relational composition.
78
Conditional, first attempt
[[if b then P else Q fi]] =
{
[[P]] if [[b]]η = true
[[Q]] otherwise.
79
Detour: Predicates as programs
A boolean expression b defines a subset (or unary relation) of Env:
〈b〉 = {η : [[b]]η = true}
This can be extended to a binary relation (i.e. a program):
[[b]] = {(η, η) : η ∈ 〈b〉}
Intuitively, b corresponds to the program
if b then skip else ⊥ fi
80
Detour: Predicates as programs
A boolean expression b defines a subset (or unary relation) of Env:
〈b〉 = {η : [[b]]η = true}
This can be extended to a binary relation (i.e. a program):
[[b]] = {(η, η) : η ∈ 〈b〉}
Intuitively, b corresponds to the program
if b then skip else ⊥ fi
81
Conditional, better attempt
[[if b then P else Q fi]] = [[b;P]] ∪ [[¬b;Q]]
82
While
while b do P od
Do 0 or more executions of P while b holds
Terminate when b does not hold
How to do “0 or more” executions of (b;P)?
83
While
while b do P od
Do 0 or more executions of (b;P)
Terminate with an execution of ¬b
How to do “0 or more” executions of (b;P)?
84
While
while b do P od
Do 0 or more executions of (b;P)
Terminate with an execution of ¬b
How to do “0 or more” executions of (b;P)?
85
Transitive closure
Given a binary relation R ⊆ E × E , the transitive closure of R, R∗
is defined to be the limit of the sequence
R0 ∪ R1 ∪ R2 · · ·
where
R0 = ∆, the diagonal relation
Rn+1 = Rn;R
NB
R∗ is the smallest transitive relation which contains R
Related to the Kleene star operation seen in languages: Σ∗
Technically, R∗ is the least-fixed point of f (X ) = X ∪ X ;R
86
Transitive closure
Given a binary relation R ⊆ E × E , the transitive closure of R, R∗
is defined to be the limit of the sequence
R0 ∪ R1 ∪ R2 · · ·
where
R0 = ∆, the diagonal relation
Rn+1 = Rn;R
NB
R∗ is the smallest transitive relation which contains R
Related to the Kleene star operation seen in languages: Σ∗
Technically, R∗ is the least-fixed point of f (X ) = X ∪ X ;R
87
While
[[while b do P od]] = [[b;P]]∗; [[¬b]]
Do 0 or more executions of (b;P)
Conclude with an execution of ¬b
88
Validity
A Hoare triple is valid, written |= {ϕ}P {ψ} if
[[P]](〈ϕ〉) ⊆ 〈ψ〉.
That is, the relational image under [[P]] of the set of states where
ϕ holds is contained in the set of states where ψ holds.
89
Validity
90
Validity
〈ϕ〉
91
Validity
〈ϕ〉 〈ψ〉
92
Validity
〈ϕ〉 〈ψ〉
[[P]]
93
Validity
〈ϕ〉 〈ψ〉[[P]](〈ϕ〉)
[[P]]
94
Soundness of Hoare Logic
Hoare Logic is sound with respect to the semantics given. That is,
Theorem
If ` {ϕ}P {ψ} then |= {ϕ}P {ψ}
95
Summary
Set theory revisited
Soundness of Hoare Logic
Completeness of Hoare Logic
96
Summary
Set theory revisited
Soundness of Hoare Logic
Completeness of Hoare Logic
97
Some results on relational images
Lemma
For any binary relations R, S ⊆ X × Y and subsets A,B ⊆ X :
(a) If A ⊆ B then R(A) ⊆ R(B)
(b) R(A) ∪ S(A) = (R ∪ S)(A)
(c) R(S(A)) = (S ;R)(A)
Proof (a):
98
Some results on relational images
Lemma
For any binary relations R, S ⊆ X × Y and subsets A,B ⊆ X :
(a) If A ⊆ B then R(A) ⊆ R(B)
(b) R(A) ∪ S(A) = (R ∪ S)(A)
(c) R(S(A)) = (S ;R)(A)
Proof (a):
99
Some results on relational images
Lemma
For any binary relations R, S ⊆ X × Y and subsets A,B ⊆ X :
(a) If A ⊆ B then R(A) ⊆ R(B)
(b) R(A) ∪ S(A) = (R ∪ S)(A)
(c) R(S(A)) = (S ;R)(A)
Proof (a):
y ∈ R(A) ⇔ ∃x ∈ A such that (x , y) ∈ R
⇒ ∃x ∈ B such that (x , y) ∈ R
⇔ y ∈ R(B)
100
Some results on relational images
Lemma
For any binary relations R, S ⊆ X × Y and subsets A,B ⊆ X :
(a) If A ⊆ B then R(A) ⊆ R(B)
(b) R(A) ∪ S(A) = (R ∪ S)(A)
(c) R(S(A)) = (S ;R)(A)
Proof (b):
101
Some results on relational images
Lemma
For any binary relations R, S ⊆ X × Y and subsets A,B ⊆ X :
(a) If A ⊆ B then R(A) ⊆ R(B)
(b) R(A) ∪ S(A) = (R ∪ S)(A)
(c) R(S(A)) = (S ;R)(A)
Proof (b):
y ∈ R(A) ∪ S(A) ⇔ y ∈ R(A) or y ∈ S(A)
⇔ ∃x ∈ A s.t. (x , y) ∈ R or ∃x ∈ A s.t. (x , y) ∈ S
⇔ ∃x ∈ A s.t. (x , y) ∈ R or (x , y) ∈ S
⇔ ∃x ∈ A s.t. (x , y) ∈ (R ∪ S)
⇔ y ∈ (R ∪ S)(A)
102
Some results on relational images
Lemma
For any binary relations R, S ⊆ X × Y and subsets A,B ⊆ X :
(a) If A ⊆ B then R(A) ⊆ R(B)
(b) R(A) ∪ S(A) = (R ∪ S)(A)
(c) R(S(A)) = (S ;R)(A)
Proof (c):
103
Some results on relational images
Lemma
For any binary relations R, S ⊆ X × Y and subsets A,B ⊆ X :
(a) If A ⊆ B then R(A) ⊆ R(B)
(b) R(A) ∪ S(A) = (R ∪ S)(A)
(c) R(S(A)) = (S ;R)(A)
Proof (c):
z ∈ R(S(A)) ⇔ ∃y ∈ S(A) s.t. (y , z) ∈ R
⇔ ∃x ∈ A, y ∈ S(A) s.t. (x , y) ∈ S and (y , z) ∈ R
⇔ ∃x ∈ A s.t. (x , z) ∈ (S ;R)
⇔ z ∈ (S ;R)(A)
104
Some results on relational images
Corollary
If R(A) ⊆ A then R∗(A) ⊆ A
Proof:
R(A) ⊆ A ⇒ R i+1(A) = R i (R(A)) ⊆ R i (A)
⇒ R i+1(A) ⊆ R(A) ⊆ A
So R∗(A) =
( ∞⋃
i=0
R i
)
(A)
=
∞⋃
i=0
R i (A)
⊆ A
105
Some results on relational images
Corollary
If R(A) ⊆ A then R∗(A) ⊆ A
Proof:
R(A) ⊆ A ⇒ R i+1(A) = R i (R(A)) ⊆ R i (A)
⇒ R i+1(A) ⊆ R(A) ⊆ A
So R∗(A) =
( ∞⋃
i=0
R i
)
(A)
=
∞⋃
i=0
R i (A)
⊆ A
106
Some results on relational images
Corollary
If R(A) ⊆ A then R∗(A) ⊆ A
Proof:
R(A) ⊆ A ⇒ R i+1(A) = R i (R(A)) ⊆ R i (A)
⇒ R i+1(A) ⊆ R(A) ⊆ A
So R∗(A) =
( ∞⋃
i=0
R i
)
(A)
=
∞⋃
i=0
R i (A)
⊆ A
107
Summary
Set theory revisited
Soundness of Hoare Logic
Completeness of Hoare Logic
108
Soundness of Hoare Logic
Theorem
If ` {ϕ}P {ψ} then |= {ϕ}P {ψ}
Proof:
By induction on the structure of the proof.
109
Soundness of Hoare Logic
Theorem
If ` {ϕ}P {ψ} then |= {ϕ}P {ψ}
Proof:
By induction on the structure of the proof.
110
Soundness of Hoare Logic
Theorem
If ` {ϕ}P {ψ} then |= {ϕ}P {ψ}
Proof:
By induction on the structure of the proof.
111
Base case: Assignment rule
(ass){ϕ[e/x ]} x := e {ϕ}
Need to show {ϕ[e/x ]} x := e {ϕ} is always valid. That is,
[[x := e]](〈ϕ[e/x ]〉) ⊆ 〈ϕ〉.
Observation: [[ϕ[e/x ]]]η = [[ϕ]]η
′
where η′ = η[x 7→ [[e]]η]
So if η ∈ 〈ϕ[e/x ]〉 then η′ ∈ 〈ϕ〉
Recall: (η, η′′) ∈ [[x := e]] if and only if η′′ = η[x 7→ [[e]]η],
So [[x := e]](η) ∈ 〈ϕ〉 for all η ∈ 〈ϕ[e/x ]〉
So [[x := e]](〈ϕ[e/x ]〉) ⊆ 〈ϕ〉
112
Base case: Assignment rule
(ass){ϕ[e/x ]} x := e {ϕ}
Need to show {ϕ[e/x ]} x := e {ϕ} is always valid. That is,
[[x := e]](〈ϕ[e/x ]〉) ⊆ 〈ϕ〉.
Observation: [[ϕ[e/x ]]]η = [[ϕ]]η
′
where η′ = η[x 7→ [[e]]η]
So if η ∈ 〈ϕ[e/x ]〉 then η′ ∈ 〈ϕ〉
Recall: (η, η′′) ∈ [[x := e]] if and only if η′′ = η[x 7→ [[e]]η],
So [[x := e]](η) ∈ 〈ϕ〉 for all η ∈ 〈ϕ[e/x ]〉
So [[x := e]](〈ϕ[e/x ]〉) ⊆ 〈ϕ〉
113
Base case: Assignment rule
(ass){ϕ[e/x ]} x := e {ϕ}
Need to show {ϕ[e/x ]} x := e {ϕ} is always valid. That is,
[[x := e]](〈ϕ[e/x ]〉) ⊆ 〈ϕ〉.
Observation: [[ϕ[e/x ]]]η = [[ϕ]]η
′
where η′ = η[x 7→ [[e]]η]
So if η ∈ 〈ϕ[e/x ]〉 then η′ ∈ 〈ϕ〉
Recall: (η, η′′) ∈ [[x := e]] if and only if η′′ = η[x 7→ [[e]]η],
So [[x := e]](η) ∈ 〈ϕ〉 for all η ∈ 〈ϕ[e/x ]〉
So [[x := e]](〈ϕ[e/x ]〉) ⊆ 〈ϕ〉
114
Base case: Assignment rule
(ass){ϕ[e/x ]} x := e {ϕ}
Need to show {ϕ[e/x ]} x := e {ϕ} is always valid. That is,
[[x := e]](〈ϕ[e/x ]〉) ⊆ 〈ϕ〉.
Observation: [[ϕ[e/x ]]]η = [[ϕ]]η
′
where η′ = η[x 7→ [[e]]η]
So if η ∈ 〈ϕ[e/x ]〉 then η′ ∈ 〈ϕ〉
Recall: (η, η′′) ∈ [[x := e]] if and only if η′′ = η[x 7→ [[e]]η],
So [[x := e]](η) ∈ 〈ϕ〉 for all η ∈ 〈ϕ[e/x ]〉
So [[x := e]](〈ϕ[e/x ]〉) ⊆ 〈ϕ〉
115
Base case: Assignment rule
(ass){ϕ[e/x ]} x := e {ϕ}
Need to show {ϕ[e/x ]} x := e {ϕ} is always valid. That is,
[[x := e]](〈ϕ[e/x ]〉) ⊆ 〈ϕ〉.
Observation: [[ϕ[e/x ]]]η = [[ϕ]]η
′
where η′ = η[x 7→ [[e]]η]
So if η ∈ 〈ϕ[e/x ]〉 then η′ ∈ 〈ϕ〉
Recall: (η, η′′) ∈ [[x := e]] if and only if η′′ = η[x 7→ [[e]]η],
So [[x := e]](η) ∈ 〈ϕ〉 for all η ∈ 〈ϕ[e/x ]〉
So [[x := e]](〈ϕ[e/x ]〉) ⊆ 〈ϕ〉
116
Base case: Assignment rule
(ass){ϕ[e/x ]} x := e {ϕ}
Need to show {ϕ[e/x ]} x := e {ϕ} is always valid. That is,
[[x := e]](〈ϕ[e/x ]〉) ⊆ 〈ϕ〉.
Observation: [[ϕ[e/x ]]]η = [[ϕ]]η
′
where η′ = η[x 7→ [[e]]η]
So if η ∈ 〈ϕ[e/x ]〉 then η′ ∈ 〈ϕ〉
Recall: (η, η′′) ∈ [[x := e]] if and only if η′′ = η[x 7→ [[e]]η],
So [[x := e]](η) ∈ 〈ϕ〉 for all η ∈ 〈ϕ[e/x ]〉
So [[x := e]](〈ϕ[e/x ]〉) ⊆ 〈ϕ〉
117
Base case: Assignment rule
(ass){ϕ[e/x ]} x := e {ϕ}
Need to show {ϕ[e/x ]} x := e {ϕ} is always valid. That is,
[[x := e]](〈ϕ[e/x ]〉) ⊆ 〈ϕ〉.
Observation: [[ϕ[e/x ]]]η = [[ϕ]]η
′
where η′ = η[x 7→ [[e]]η]
So if η ∈ 〈ϕ[e/x ]〉 then η′ ∈ 〈ϕ〉
Recall: (η, η′′) ∈ [[x := e]] if and only if η′′ = η[x 7→ [[e]]η],
So [[x := e]](η) ∈ 〈ϕ〉 for all η ∈ 〈ϕ[e/x ]〉
So [[x := e]](〈ϕ[e/x ]〉) ⊆ 〈ϕ〉
118
Inductive case 1: Sequence rule
{ϕ}P {ψ} {ψ}Q {ρ}
(seq){ϕ}P;Q {ρ}
Assume {ϕ}P {ψ} and {ψ}Q {ρ} are valid. Need to show that
{ϕ}P;Q {ρ} is valid.
Recall: [[P;Q]] = [[P]]; [[Q]]
So: [[P;Q]](〈ϕ〉) = [[Q]]([[P]](〈ϕ〉)) (see Lemma 1(c))
By IH: [[P]](〈ϕ〉) ⊆ 〈ψ〉 and [[Q]](〈ψ〉) ⊆ 〈ρ〉
So: [[Q]]
(
[[P]](〈ϕ〉)) ⊆ [[Q]](〈ψ〉) ⊆ 〈ρ〉 (see Lemma 1(a))
119
Inductive case 1: Sequence rule
{ϕ}P {ψ} {ψ}Q {ρ}
(seq){ϕ}P;Q {ρ}
Assume {ϕ}P {ψ} and {ψ}Q {ρ} are valid. Need to show that
{ϕ}P;Q {ρ} is valid.
Recall: [[P;Q]] = [[P]]; [[Q]]
So: [[P;Q]](〈ϕ〉) = [[Q]]([[P]](〈ϕ〉)) (see Lemma 1(c))
By IH: [[P]](〈ϕ〉) ⊆ 〈ψ〉 and [[Q]](〈ψ〉) ⊆ 〈ρ〉
So: [[Q]]
(
[[P]](〈ϕ〉)) ⊆ [[Q]](〈ψ〉) ⊆ 〈ρ〉 (see Lemma 1(a))
120
Inductive case 1: Sequence rule
{ϕ}P {ψ} {ψ}Q {ρ}
(seq){ϕ}P;Q {ρ}
Assume {ϕ}P {ψ} and {ψ}Q {ρ} are valid. Need to show that
{ϕ}P;Q {ρ} is valid.
Recall: [[P;Q]] = [[P]]; [[Q]]
So: [[P;Q]](〈ϕ〉) = [[Q]]([[P]](〈ϕ〉)) (see Lemma 1(c))
By IH: [[P]](〈ϕ〉) ⊆ 〈ψ〉 and [[Q]](〈ψ〉) ⊆ 〈ρ〉
So: [[Q]]
(
[[P]](〈ϕ〉)) ⊆ [[Q]](〈ψ〉) ⊆ 〈ρ〉 (see Lemma 1(a))
121
Inductive case 1: Sequence rule
{ϕ}P {ψ} {ψ}Q {ρ}
(seq){ϕ}P;Q {ρ}
Assume {ϕ}P {ψ} and {ψ}Q {ρ} are valid. Need to show that
{ϕ}P;Q {ρ} is valid.
Recall: [[P;Q]] = [[P]]; [[Q]]
So: [[P;Q]](〈ϕ〉) = [[Q]]([[P]](〈ϕ〉)) (see Lemma 1(c))
By IH: [[P]](〈ϕ〉) ⊆ 〈ψ〉 and [[Q]](〈ψ〉) ⊆ 〈ρ〉
So: [[Q]]
(
[[P]](〈ϕ〉)) ⊆ [[Q]](〈ψ〉) ⊆ 〈ρ〉 (see Lemma 1(a))
122
Inductive case 1: Sequence rule
{ϕ}P {ψ} {ψ}Q {ρ}
(seq){ϕ}P;Q {ρ}
Assume {ϕ}P {ψ} and {ψ}Q {ρ} are valid. Need to show that
{ϕ}P;Q {ρ} is valid.
Recall: [[P;Q]] = [[P]]; [[Q]]
So: [[P;Q]](〈ϕ〉) = [[Q]]([[P]](〈ϕ〉)) (see Lemma 1(c))
By IH: [[P]](〈ϕ〉) ⊆ 〈ψ〉 and [[Q]](〈ψ〉) ⊆ 〈ρ〉
So: [[Q]]
(
[[P]](〈ϕ〉)) ⊆ [[Q]](〈ψ〉) ⊆ 〈ρ〉 (see Lemma 1(a))
123
Inductive case 1: Sequence rule
{ϕ}P {ψ} {ψ}Q {ρ}
(seq){ϕ}P;Q {ρ}
Assume {ϕ}P {ψ} and {ψ}Q {ρ} are valid. Need to show that
{ϕ}P;Q {ρ} is valid.
Recall: [[P;Q]] = [[P]]; [[Q]]
So: [[P;Q]](〈ϕ〉) = [[Q]]([[P]](〈ϕ〉)) (see Lemma 1(c))
By IH: [[P]](〈ϕ〉) ⊆ 〈ψ〉 and [[Q]](〈ψ〉) ⊆ 〈ρ〉
So: [[Q]]
(
[[P]](〈ϕ〉)) ⊆ [[Q]](〈ψ〉) ⊆ 〈ρ〉 (see Lemma 1(a))
124
Two more useful results
Lemma
For R ⊆ Env×Env, predicates ϕ and ψ, and X ⊆ Env:
(a) [[ϕ]](X ) = 〈ϕ〉 ∩ X
(b) R(〈ϕ ∧ ψ〉) = ([[ϕ]];R)(〈ψ〉))
Proof (a):
125
Two more useful results
Lemma
For R ⊆ Env×Env, predicates ϕ and ψ, and X ⊆ Env:
(a) [[ϕ]](X ) = 〈ϕ〉 ∩ X
(b) R(〈ϕ ∧ ψ〉) = ([[ϕ]];R)(〈ψ〉))
Proof (a):
126
Two more useful results
Lemma
For R ⊆ Env×Env, predicates ϕ and ψ, and X ⊆ Env:
(a) [[ϕ]](X ) = 〈ϕ〉 ∩ X
(b) R(〈ϕ ∧ ψ〉) = ([[ϕ]];R)(〈ψ〉))
Proof (a):
η′ ∈ [[ϕ]](X ) ⇔ ∃η ∈ X s.t. (η, η′) ∈ [[ϕ]]
⇔ ∃η ∈ X s.t. η = η′ and η ∈ 〈ϕ〉
⇔ η′ ∈ X ∩ 〈ϕ〉
127
Two more useful results
Lemma
For R ⊆ Env×Env, predicates ϕ and ψ, and X ⊆ Env:
(a) [[ϕ]](X ) = 〈ϕ〉 ∩ X
(b) R(〈ϕ ∧ ψ〉) = ([[ϕ]];R)(〈ψ〉))
Proof (b):
〈ϕ ∧ ψ〉 = 〈ϕ〉 ∩ 〈ψ〉 = [[ϕ]](〈ψ〉)
So R(〈ϕ ∧ ψ〉) = R([[ϕ]](〈ψ〉))
= ([[ϕ]];R)(〈ψ〉) (see Lemma 1(b))
128
Inductive case 2: Conditional rule
{ϕ ∧ g}P {ψ} {ϕ ∧ ¬g}Q {ψ}
(if){ϕ} if g then P else Q fi {ψ}
Assume {ϕ ∧ g}P {ψ} and {ϕ ∧ ¬g}Q {ψ} are valid. Need to
show that {ϕ} if g then P else Q fi {ψ} is valid.
Recall: [[if g then P else Q fi]] = [[g ;P]] ∪ [[¬g ;Q]]
[[if g then P else Q fi]](〈ϕ〉)
= [[g ;P]](〈ϕ〉) ∪ [[¬g ;Q]](〈ϕ〉) (see Lemma 1(b))
= [[P]](〈g ∧ ϕ〉) ∪ [[Q]](〈¬g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ψ〉 (by IH)
129
Inductive case 2: Conditional rule
{ϕ ∧ g}P {ψ} {ϕ ∧ ¬g}Q {ψ}
(if){ϕ} if g then P else Q fi {ψ}
Assume {ϕ ∧ g}P {ψ} and {ϕ ∧ ¬g}Q {ψ} are valid. Need to
show that {ϕ} if g then P else Q fi {ψ} is valid.
Recall: [[if g then P else Q fi]] = [[g ;P]] ∪ [[¬g ;Q]]
[[if g then P else Q fi]](〈ϕ〉)
= [[g ;P]](〈ϕ〉) ∪ [[¬g ;Q]](〈ϕ〉) (see Lemma 1(b))
= [[P]](〈g ∧ ϕ〉) ∪ [[Q]](〈¬g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ψ〉 (by IH)
130
Inductive case 2: Conditional rule
{ϕ ∧ g}P {ψ} {ϕ ∧ ¬g}Q {ψ}
(if){ϕ} if g then P else Q fi {ψ}
Assume {ϕ ∧ g}P {ψ} and {ϕ ∧ ¬g}Q {ψ} are valid. Need to
show that {ϕ} if g then P else Q fi {ψ} is valid.
Recall: [[if g then P else Q fi]] = [[g ;P]] ∪ [[¬g ;Q]]
[[if g then P else Q fi]](〈ϕ〉)
= [[g ;P]](〈ϕ〉) ∪ [[¬g ;Q]](〈ϕ〉) (see Lemma 1(b))
= [[P]](〈g ∧ ϕ〉) ∪ [[Q]](〈¬g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ψ〉 (by IH)
131
Inductive case 2: Conditional rule
{ϕ ∧ g}P {ψ} {ϕ ∧ ¬g}Q {ψ}
(if){ϕ} if g then P else Q fi {ψ}
Assume {ϕ ∧ g}P {ψ} and {ϕ ∧ ¬g}Q {ψ} are valid. Need to
show that {ϕ} if g then P else Q fi {ψ} is valid.
Recall: [[if g then P else Q fi]] = [[g ;P]] ∪ [[¬g ;Q]]
[[if g then P else Q fi]](〈ϕ〉)
= [[g ;P]](〈ϕ〉) ∪ [[¬g ;Q]](〈ϕ〉) (see Lemma 1(b))
= [[P]](〈g ∧ ϕ〉) ∪ [[Q]](〈¬g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ψ〉 (by IH)
132
Inductive case 2: Conditional rule
{ϕ ∧ g}P {ψ} {ϕ ∧ ¬g}Q {ψ}
(if){ϕ} if g then P else Q fi {ψ}
Assume {ϕ ∧ g}P {ψ} and {ϕ ∧ ¬g}Q {ψ} are valid. Need to
show that {ϕ} if g then P else Q fi {ψ} is valid.
Recall: [[if g then P else Q fi]] = [[g ;P]] ∪ [[¬g ;Q]]
[[if g then P else Q fi]](〈ϕ〉)
= [[g ;P]](〈ϕ〉) ∪ [[¬g ;Q]](〈ϕ〉) (see Lemma 1(b))
= [[P]](〈g ∧ ϕ〉) ∪ [[Q]](〈¬g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ψ〉 (by IH)
133
Inductive case 2: Conditional rule
{ϕ ∧ g}P {ψ} {ϕ ∧ ¬g}Q {ψ}
(if){ϕ} if g then P else Q fi {ψ}
Assume {ϕ ∧ g}P {ψ} and {ϕ ∧ ¬g}Q {ψ} are valid. Need to
show that {ϕ} if g then P else Q fi {ψ} is valid.
Recall: [[if g then P else Q fi]] = [[g ;P]] ∪ [[¬g ;Q]]
[[if g then P else Q fi]](〈ϕ〉)
= [[g ;P]](〈ϕ〉) ∪ [[¬g ;Q]](〈ϕ〉) (see Lemma 1(b))
= [[P]](〈g ∧ ϕ〉) ∪ [[Q]](〈¬g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ψ〉 (by IH)
134
Inductive case 2: Conditional rule
{ϕ ∧ g}P {ψ} {ϕ ∧ ¬g}Q {ψ}
(if){ϕ} if g then P else Q fi {ψ}
Assume {ϕ ∧ g}P {ψ} and {ϕ ∧ ¬g}Q {ψ} are valid. Need to
show that {ϕ} if g then P else Q fi {ψ} is valid.
Recall: [[if g then P else Q fi]] = [[g ;P]] ∪ [[¬g ;Q]]
[[if g then P else Q fi]](〈ϕ〉)
= [[g ;P]](〈ϕ〉) ∪ [[¬g ;Q]](〈ϕ〉) (see Lemma 1(b))
= [[P]](〈g ∧ ϕ〉) ∪ [[Q]](〈¬g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ψ〉 (by IH)
135
Inductive case 3: While rule
{ϕ ∧ g}P {ϕ}
(loop){ϕ}while g do P od {ϕ ∧ ¬g}
Assume {ϕ ∧ g}P {ϕ} is valid. Need to show that
{ϕ}while g do P od {ϕ ∧ ¬g}is valid.
Recall: [[while g do P od]] = [[g ;P]]∗; [[¬g ]]
[[g ;P]](〈ϕ〉) = [[P]](〈g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ϕ〉 (IH)
So [[g ;P]]∗(〈ϕ〉) ⊆ 〈ϕ〉 (see Corollary)
So [[g ;P]]∗; [[¬g ]](〈ϕ〉) = [[¬g ]]([[g ;P]]∗(〈ϕ〉)) (see Lemma 1(c))
⊆ [[¬g ]](〈ϕ〉) (see Lemma 1(a))
= 〈¬g ∧ ϕ〉 (see Lemma 2(a))
136
Inductive case 3: While rule
{ϕ ∧ g}P {ϕ}
(loop){ϕ}while g do P od {ϕ ∧ ¬g}
Assume {ϕ ∧ g}P {ϕ} is valid. Need to show that
{ϕ}while g do P od {ϕ ∧ ¬g}is valid.
Recall: [[while g do P od]] = [[g ;P]]∗; [[¬g ]]
[[g ;P]](〈ϕ〉) = [[P]](〈g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ϕ〉 (IH)
So [[g ;P]]∗(〈ϕ〉) ⊆ 〈ϕ〉 (see Corollary)
So [[g ;P]]∗; [[¬g ]](〈ϕ〉) = [[¬g ]]([[g ;P]]∗(〈ϕ〉)) (see Lemma 1(c))
⊆ [[¬g ]](〈ϕ〉) (see Lemma 1(a))
= 〈¬g ∧ ϕ〉 (see Lemma 2(a))
137
Inductive case 3: While rule
{ϕ ∧ g}P {ϕ}
(loop){ϕ}while g do P od {ϕ ∧ ¬g}
Assume {ϕ ∧ g}P {ϕ} is valid. Need to show that
{ϕ}while g do P od {ϕ ∧ ¬g}is valid.
Recall: [[while g do P od]] = [[g ;P]]∗; [[¬g ]]
[[g ;P]](〈ϕ〉) = [[P]](〈g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ϕ〉 (IH)
So [[g ;P]]∗(〈ϕ〉) ⊆ 〈ϕ〉 (see Corollary)
So [[g ;P]]∗; [[¬g ]](〈ϕ〉) = [[¬g ]]([[g ;P]]∗(〈ϕ〉)) (see Lemma 1(c))
⊆ [[¬g ]](〈ϕ〉) (see Lemma 1(a))
= 〈¬g ∧ ϕ〉 (see Lemma 2(a))
138
Inductive case 3: While rule
{ϕ ∧ g}P {ϕ}
(loop){ϕ}while g do P od {ϕ ∧ ¬g}
Assume {ϕ ∧ g}P {ϕ} is valid. Need to show that
{ϕ}while g do P od {ϕ ∧ ¬g}is valid.
Recall: [[while g do P od]] = [[g ;P]]∗; [[¬g ]]
[[g ;P]](〈ϕ〉) = [[P]](〈g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ϕ〉 (IH)
So [[g ;P]]∗(〈ϕ〉) ⊆ 〈ϕ〉 (see Corollary)
So [[g ;P]]∗; [[¬g ]](〈ϕ〉) = [[¬g ]]([[g ;P]]∗(〈ϕ〉)) (see Lemma 1(c))
⊆ [[¬g ]](〈ϕ〉) (see Lemma 1(a))
= 〈¬g ∧ ϕ〉 (see Lemma 2(a))
139
Inductive case 3: While rule
{ϕ ∧ g}P {ϕ}
(loop){ϕ}while g do P od {ϕ ∧ ¬g}
Assume {ϕ ∧ g}P {ϕ} is valid. Need to show that
{ϕ}while g do P od {ϕ ∧ ¬g}is valid.
Recall: [[while g do P od]] = [[g ;P]]∗; [[¬g ]]
[[g ;P]](〈ϕ〉) = [[P]](〈g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ϕ〉 (IH)
So [[g ;P]]∗(〈ϕ〉) ⊆ 〈ϕ〉 (see Corollary)
So [[g ;P]]∗; [[¬g ]](〈ϕ〉) = [[¬g ]]([[g ;P]]∗(〈ϕ〉)) (see Lemma 1(c))
⊆ [[¬g ]](〈ϕ〉) (see Lemma 1(a))
= 〈¬g ∧ ϕ〉 (see Lemma 2(a))
140
Inductive case 3: While rule
{ϕ ∧ g}P {ϕ}
(loop){ϕ}while g do P od {ϕ ∧ ¬g}
Assume {ϕ ∧ g}P {ϕ} is valid. Need to show that
{ϕ}while g do P od {ϕ ∧ ¬g}is valid.
Recall: [[while g do P od]] = [[g ;P]]∗; [[¬g ]]
[[g ;P]](〈ϕ〉) = [[P]](〈g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ϕ〉 (IH)
So [[g ;P]]∗(〈ϕ〉) ⊆ 〈ϕ〉 (see Corollary)
So [[g ;P]]∗; [[¬g ]](〈ϕ〉) = [[¬g ]]([[g ;P]]∗(〈ϕ〉)) (see Lemma 1(c))
⊆ [[¬g ]](〈ϕ〉) (see Lemma 1(a))
= 〈¬g ∧ ϕ〉 (see Lemma 2(a))
141
Inductive case 3: While rule
{ϕ ∧ g}P {ϕ}
(loop){ϕ}while g do P od {ϕ ∧ ¬g}
Assume {ϕ ∧ g}P {ϕ} is valid. Need to show that
{ϕ}while g do P od {ϕ ∧ ¬g}is valid.
Recall: [[while g do P od]] = [[g ;P]]∗; [[¬g ]]
[[g ;P]](〈ϕ〉) = [[P]](〈g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ϕ〉 (IH)
So [[g ;P]]∗(〈ϕ〉) ⊆ 〈ϕ〉 (see Corollary)
So [[g ;P]]∗; [[¬g ]](〈ϕ〉) = [[¬g ]]([[g ;P]]∗(〈ϕ〉)) (see Lemma 1(c))
⊆ [[¬g ]](〈ϕ〉) (see Lemma 1(a))
= 〈¬g ∧ ϕ〉 (see Lemma 2(a))
142
Inductive case 3: While rule
{ϕ ∧ g}P {ϕ}
(loop){ϕ}while g do P od {ϕ ∧ ¬g}
Assume {ϕ ∧ g}P {ϕ} is valid. Need to show that
{ϕ}while g do P od {ϕ ∧ ¬g}is valid.
Recall: [[while g do P od]] = [[g ;P]]∗; [[¬g ]]
[[g ;P]](〈ϕ〉) = [[P]](〈g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ϕ〉 (IH)
So [[g ;P]]∗(〈ϕ〉) ⊆ 〈ϕ〉 (see Corollary)
So [[g ;P]]∗; [[¬g ]](〈ϕ〉) = [[¬g ]]([[g ;P]]∗(〈ϕ〉)) (see Lemma 1(c))
⊆ [[¬g ]](〈ϕ〉) (see Lemma 1(a))
= 〈¬g ∧ ϕ〉 (see Lemma 2(a))
143
Inductive case 3: While rule
{ϕ ∧ g}P {ϕ}
(loop){ϕ}while g do P od {ϕ ∧ ¬g}
Assume {ϕ ∧ g}P {ϕ} is valid. Need to show that
{ϕ}while g do P od {ϕ ∧ ¬g}is valid.
Recall: [[while g do P od]] = [[g ;P]]∗; [[¬g ]]
[[g ;P]](〈ϕ〉) = [[P]](〈g ∧ ϕ〉) (see Lemma 2(b))
⊆ 〈ϕ〉 (IH)
So [[g ;P]]∗(〈ϕ〉) ⊆ 〈ϕ〉 (see Corollary)
So [[g ;P]]∗; [[¬g ]](〈ϕ〉) = [[¬g ]]([[g ;P]]∗(〈ϕ〉)) (see Lemma 1(c))
⊆ [[¬g ]](〈ϕ〉) (see Lemma 1(a))
= 〈¬g ∧ ϕ〉 (see Lemma 2(a))
144
Inductive case 4: Consequence rule
ϕ′ → ϕ {ϕ}P {ψ} ψ → ψ′
(cons){ϕ′}P {ψ′}
Assume {ϕ}P {ψ} is valid and ϕ′ → ϕ and ψ → ψ′. Need to show
that {ϕ′}P {ψ′} is valid.
Observe: If ϕ′ → ϕ then 〈ϕ′〉 ⊆ 〈ϕ〉
[[P]](〈ϕ′〉) ⊆ [[P]](〈ϕ〉) (see Lemma 1(a))
⊆ 〈ψ〉 (IH)
⊆ 〈ψ′〉
145
Inductive case 4: Consequence rule
ϕ′ → ϕ {ϕ}P {ψ} ψ → ψ′
(cons){ϕ′}P {ψ′}
Assume {ϕ}P {ψ} is valid and ϕ′ → ϕ and ψ → ψ′. Need to show
that {ϕ′}P {ψ′} is valid.
Observe: If ϕ′ → ϕ then 〈ϕ′〉 ⊆ 〈ϕ〉
[[P]](〈ϕ′〉) ⊆ [[P]](〈ϕ〉) (see Lemma 1(a))
⊆ 〈ψ〉 (IH)
⊆ 〈ψ′〉
146
Inductive case 4: Consequence rule
ϕ′ → ϕ {ϕ}P {ψ} ψ → ψ′
(cons){ϕ′}P {ψ′}
Assume {ϕ}P {ψ} is valid and ϕ′ → ϕ and ψ → ψ′. Need to show
that {ϕ′}P {ψ′} is valid.
Observe: If ϕ′ → ϕ then 〈ϕ′〉 ⊆ 〈ϕ〉
[[P]](〈ϕ′〉) ⊆ [[P]](〈ϕ〉) (see Lemma 1(a))
⊆ 〈ψ〉 (IH)
⊆ 〈ψ′〉
147
Inductive case 4: Consequence rule
ϕ′ → ϕ {ϕ}P {ψ} ψ → ψ′
(cons){ϕ′}P {ψ′}
Assume {ϕ}P {ψ} is valid and ϕ′ → ϕ and ψ → ψ′. Need to show
that {ϕ′}P {ψ′} is valid.
Observe: If ϕ′ → ϕ then 〈ϕ′〉 ⊆ 〈ϕ〉
[[P]](〈ϕ′〉) ⊆ [[P]](〈ϕ〉) (see Lemma 1(a))
⊆ 〈ψ〉 (IH)
⊆ 〈ψ′〉
148
Inductive case 4: Consequence rule
ϕ′ → ϕ {ϕ}P {ψ} ψ → ψ′
(cons){ϕ′}P {ψ′}
Assume {ϕ}P {ψ} is valid and ϕ′ → ϕ and ψ → ψ′. Need to show
that {ϕ′}P {ψ′} is valid.
Observe: If ϕ′ → ϕ then 〈ϕ′〉 ⊆ 〈ϕ〉
[[P]](〈ϕ′〉) ⊆ [[P]](〈ϕ〉) (see Lemma 1(a))
⊆ 〈ψ〉 (IH)
⊆ 〈ψ′〉
149
Soundness of Hoare Logic
Theorem
If ` {ϕ}P {ψ} then |= {ϕ}P {ψ}
150
Summary
Set theory revisited
Soundness of Hoare Logic
Completeness of Hoare Logic
151
Incompleteness
Theorem (Go¨del’s Incompleteness Theorem)
There is no proof system that can prove every valid first-order
sentence about arithmetic over the natural numbers.
⇒ There are true statements that do not have a proof.
⇒ Because of (cons) there are valid triples that result from valid,
but unprovable, consequences.
⇒ Hoare Logic is not complete.
152
Incompleteness
Theorem (Go¨del’s Incompleteness Theorem)
There is no proof system that can prove every valid first-order
sentence about arithmetic over the natural numbers.
⇒ There are true statements that do not have a proof.
⇒ Because of (cons) there are valid triples that result from valid,
but unprovable, consequences.
⇒ Hoare Logic is not complete.
153
Incompleteness
Theorem (Go¨del’s Incompleteness Theorem)
There is no proof system that can prove every valid first-order
sentence about arithmetic over the natural numbers.
⇒ There are true statements that do not have a proof.
⇒ Because of (cons) there are valid triples that result from valid,
but unprovable, consequences.
⇒ Hoare Logic is not complete.
154
Incompleteness
Theorem (Go¨del’s Incompleteness Theorem)
There is no proof system that can prove every valid first-order
sentence about arithmetic over the natural numbers.
⇒ There are true statements that do not have a proof.
⇒ Because of (cons) there are valid triples that result from valid,
but unprovable, consequences.
⇒ Hoare Logic is not complete.
155
Relative completeness of Hoare Logic
Theorem (Relative completeness of Hoare Logic)
With an oracle that decides the validity of predicates,
if |= {ϕ}P {ψ} then ` {ϕ}P {ψ} .
156
Need to know for this course
Write programs in L.
Give proofs using the Hoare logic rules (full and outline)
Definition of [[·]]
Definition of composition and transitive closure
