History TinyImp Hoare Logic
Imperative Programming Languages
Dr. Liam O’Connor
University of Edinburgh LFCS UNSW, Term 3 2020
1
History
TinyImp Hoare Logic
Imperative Programming
imper ̄o
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).
2
History TinyImp Hoare Logic
The Old Days
Early microcomputer languages used a line numbering system with GO TO statements used to arrange control flow.
3
History TinyImp Hoare Logic
Factorial Example in BASIC (1964)
4
History TinyImp Hoare Logic
Dijkstra (1968)
The structured programming movement brought in control structures to mainstream use, such as conditionals and loops.
5
History TinyImp Hoare Logic
Factorial Example in Pascal (1970)
6
History
TinyImp Hoare Logic
Syntax
We’re going to specify a language TinyImp, based on structured programming. The syntax consists of statements and expressions.
Grammar
Stmt ::= |
| | | |
Expr ::=
skip
x := Expr
var y · Stmt
if Expr then Stmt else Stmt fi while Expr do Stmt od
Stmt ; Stmt
⟨Arithmetic expressions⟩
Do nothing Assignment Declaration Conditional
Loop Sequencing
We already know how to make unambiguous abstract syntax, so we will use concrete syntax in the rules for readability.
7
History
TinyImp
Hoare Logic
Examples
Example (Factorial and Fibonacci)
var i ·
var m ·
i := 0;
m := 1;
while i < N do
i := i + 1;
m := m × i od
var m·var n·var i · m := 1; n := 1;
i := 1;
while i < N do
var t · t := m; m := n;
n := m + t;
i := i + 1
od
8
History
TinyImp Hoare Logic
Types?
Static Semantics
9
History TinyImp Hoare Logic
Static Semantics
Types? We only have one type (int), so type checking is a wash.
Scopes?
10
History
TinyImp
Hoare Logic
Static Semantics
Types? We only have one type (int), so type checking is a wash.
Scopes? We have to check that variables are declared before use. Anything Else?
11
History
TinyImp Hoare Logic
Static Semantics
Types? We only have one type (int), so type checking is a wash.
Scopes? We have to check that variables are declared before use.
Anything Else? We have to check that variables are initialized before they are used!
12
History
TinyImp Hoare Logic
Static Semantics
Types? We only have one type (int), so type checking is a wash.
Scopes? We have to check that variables are declared before use.
Anything Else? We have to check that variables are initialized before they are used!
Note: V ⊆ U
U;V ⊢s okW
13
History
TinyImp Hoare Logic
Static Semantics
Types? We only have one type (int), so type checking is a wash.
Scopes? We have to check that variables are declared before use.
Anything Else? We have to check that variables are initialized before they are used!
U;V ⊢s okW
Note: V ⊆ U
14
Set of declared free variables
History
TinyImp Hoare Logic
Static Semantics
Types? We only have one type (int), so type checking is a wash.
Scopes? We have to check that variables are declared before use.
Anything Else? We have to check that variables are initialized before they are used!
Set of initialized free variables
U;V ⊢s okW
Note: V ⊆ U
Set of declared free variables
15
History
TinyImp Hoare Logic
Static Semantics
Types? We only have one type (int), so type checking is a wash.
Scopes? We have to check that variables are declared before use.
Anything Else? We have to check that variables are initialized before they are used!
Note: V ⊆ U
U;V ⊢s okW
16
Set of initialized free variables
Indicates that no unsafe reads occur
Set of declared free variables
History
TinyImp Hoare Logic
Static Semantics
Types? We only have one type (int), so type checking is a wash.
Scopes? We have to check that variables are declared before use.
Anything Else? We have to check that variables are initialized before they are used!
Note: V ⊆ U
Indicates that no unsafe reads occur
Set of initialized free variables
U;V ⊢s okW
Set of declared free variables
Set of definitely written to free variables
17
History TinyImp Hoare Logic
Static Semantics Rules
U;V ⊢ skip ok ∅
18
History TinyImp Hoare Logic
Static Semantics Rules
U;V ⊢skipok∅ U;V ⊢x :=e ok
19
History TinyImp Hoare Logic
Static Semantics Rules
x∈U
U;V ⊢skipok∅ U;V ⊢x :=e ok
20
History TinyImp Hoare Logic
Static Semantics Rules
x ∈ U FV(e) ⊆ V U;V ⊢skipok∅ U;V ⊢x :=e ok
21
History TinyImp Hoare Logic
Static Semantics Rules
x ∈ U FV(e) ⊆ V U;V ⊢skipok∅ U;V ⊢x :=e ok{x}
22
History
TinyImp
Hoare Logic
Static Semantics Rules
x ∈ U FV(e) ⊆ V U;V ⊢skipok∅ U;V ⊢x :=e ok{x}
U; V ⊢ var y · s ok
23
History
TinyImp
Hoare Logic
Static Semantics Rules
x ∈ U FV(e) ⊆ V U;V ⊢skipok∅ U;V ⊢x :=e ok{x}
U ∪ {y }; V ⊢ s ok W U; V ⊢ var y · s ok
24
History
TinyImp
Hoare Logic
Static Semantics Rules
x ∈ U FV(e) ⊆ V U;V ⊢skipok∅ U;V ⊢x :=e ok{x}
U ∪ {y }; V ⊢ s ok W
U ; V ⊢ var y · s ok W \ {y }
25
History
TinyImp
Hoare Logic
Static Semantics Rules
x ∈ U FV(e) ⊆ V U;V ⊢skipok∅ U;V ⊢x :=e ok{x}
U ∪ {y }; V ⊢ s ok W
U ; V ⊢ var y · s ok W \ {y }
U;V ⊢ife thens1 elses2 fiok
26
History
TinyImp
Hoare Logic
Static Semantics Rules
x ∈ U FV(e) ⊆ V U;V ⊢skipok∅ U;V ⊢x :=e ok{x}
U ∪ {y }; V ⊢ s ok W
U ; V ⊢ var y · s ok W \ {y }
FV(e) ⊆ V
U;V ⊢ife thens1 elses2 fiok
27
History
TinyImp
Hoare Logic
Static Semantics Rules
x ∈ U FV(e) ⊆ V U;V ⊢skipok∅ U;V ⊢x :=e ok{x}
U ∪ {y }; V ⊢ s ok W
U ; V ⊢ var y · s ok W \ {y }
FV(e)⊆V U;V ⊢s1 okW1
U;V ⊢ife thens1 elses2 fiok
28
History
TinyImp
Hoare Logic
Static Semantics Rules
x ∈ U FV(e) ⊆ V U;V ⊢skipok∅ U;V ⊢x :=e ok{x}
U ∪ {y }; V ⊢ s ok W
U ; V ⊢ var y · s ok W \ {y }
FV(e)⊆V U;V ⊢s1 okW1 U;V ⊢s2 okW2
U;V ⊢ife thens1 elses2 fiok
29
History
TinyImp
Hoare Logic
Static Semantics Rules
x ∈ U FV(e) ⊆ V U;V ⊢skipok∅ U;V ⊢x :=e ok{x}
U ∪ {y }; V ⊢ s ok W
U ; V ⊢ var y · s ok W \ {y }
FV(e)⊆V U;V ⊢s1 okW1 U;V ⊢s2 okW2 U; V ⊢ if e then s1 else s2 fi ok W1 ∩ W2
30
History
TinyImp
Hoare Logic
Static Semantics Rules
x ∈ U FV(e) ⊆ V U;V ⊢skipok∅ U;V ⊢x :=e ok{x}
U ∪ {y }; V ⊢ s ok W
U ; V ⊢ var y · s ok W \ {y }
FV(e)⊆V U;V ⊢s1 okW1 U;V ⊢s2 okW2 U; V ⊢ if e then s1 else s2 fi ok W1 ∩ W2
U;V ⊢whilee dos odok
31
History
TinyImp
Hoare Logic
Static Semantics Rules
x ∈ U FV(e) ⊆ V U;V ⊢skipok∅ U;V ⊢x :=e ok{x}
U ∪ {y }; V ⊢ s ok W
U ; V ⊢ var y · s ok W \ {y }
FV(e)⊆V U;V ⊢s1 okW1 U;V ⊢s2 okW2 U; V ⊢ if e then s1 else s2 fi ok W1 ∩ W2
FV(e) ⊆ V
U;V ⊢whilee dos odok
32
History
TinyImp
Hoare Logic
Static Semantics Rules
x ∈ U FV(e) ⊆ V U;V ⊢skipok∅ U;V ⊢x :=e ok{x}
U ∪ {y }; V ⊢ s ok W
U ; V ⊢ var y · s ok W \ {y }
FV(e)⊆V U;V ⊢s1 okW1 U;V ⊢s2 okW2 U; V ⊢ if e then s1 else s2 fi ok W1 ∩ W2 FV(e)⊆V U;V ⊢s okW
U;V ⊢whilee dos odok
33
History
TinyImp
Hoare Logic
Static Semantics Rules
x ∈ U FV(e) ⊆ V U;V ⊢skipok∅ U;V ⊢x :=e ok{x}
U ∪ {y }; V ⊢ s ok W
U ; V ⊢ var y · s ok W \ {y }
FV(e)⊆V U;V ⊢s1 okW1 U;V ⊢s2 okW2 U; V ⊢ if e then s1 else s2 fi ok W1 ∩ W2 FV(e)⊆V U;V ⊢s okW
U;V ⊢whilee dos odok∅
34
History
TinyImp
Hoare Logic
Static Semantics Rules
x ∈ U FV(e) ⊆ V U;V ⊢skipok∅ U;V ⊢x :=e ok{x}
U ∪ {y }; V ⊢ s ok W
U ; V ⊢ var y · s ok W \ {y }
FV(e)⊆V U;V ⊢s1 okW1 U;V ⊢s2 okW2 U; V ⊢ if e then s1 else s2 fi ok W1 ∩ W2 FV(e)⊆V U;V ⊢s okW
U;V ⊢whilee dos odok∅
U;V ⊢s1;s2 ok
35
History
TinyImp
Hoare Logic
Static Semantics Rules
x ∈ U FV(e) ⊆ V U;V ⊢skipok∅ U;V ⊢x :=e ok{x}
U ∪ {y }; V ⊢ s ok W
U ; V ⊢ var y · s ok W \ {y }
FV(e)⊆V U;V ⊢s1 okW1 U;V ⊢s2 okW2 U; V ⊢ if e then s1 else s2 fi ok W1 ∩ W2 FV(e)⊆V U;V ⊢s okW
U;V ⊢whilee dos odok∅
U;V ⊢s1 okW1
U;V ⊢s1;s2 ok
36
History
TinyImp
Hoare Logic
Static Semantics Rules
x ∈ U FV(e) ⊆ V U;V ⊢skipok∅ U;V ⊢x :=e ok{x}
U ∪ {y }; V ⊢ s ok W
U ; V ⊢ var y · s ok W \ {y }
FV(e)⊆V U;V ⊢s1 okW1 U;V ⊢s2 okW2 U; V ⊢ if e then s1 else s2 fi ok W1 ∩ W2 FV(e)⊆V U;V ⊢s okW
U;V ⊢whilee dos odok∅
U;V ⊢s1 okW1 U;(V ∪W1)⊢s2 okW2
U;V ⊢s1;s2 ok
37
History
TinyImp
Hoare Logic
Static Semantics Rules
x ∈ U FV(e) ⊆ V U;V ⊢skipok∅ U;V ⊢x :=e ok{x}
U ∪ {y }; V ⊢ s ok W
U ; V ⊢ var y · s ok W \ {y }
FV(e)⊆V U;V ⊢s1 okW1 U;V ⊢s2 okW2 U; V ⊢ if e then s1 else s2 fi ok W1 ∩ W2 FV(e)⊆V U;V ⊢s okW
U;V ⊢whilee dos odok∅
U;V ⊢s1 okW1 U;(V ∪W1)⊢s2 okW2 U;V ⊢s1;s2 okW1 ∪W2
38
History TinyImp Hoare Logic
Dynamic Semantics
We will use big-step operational semantics. What are the sets of evaluable expressions and values here?
39
History
TinyImp Hoare Logic
Dynamic Semantics
We will use big-step operational semantics. What are the sets of evaluable expressions and values here?
Evaluable Expressions:
40
History
TinyImp Hoare Logic
Dynamic Semantics
We will use big-step operational semantics. What are the sets of evaluable expressions and values here?
Evaluable Expressions: A pair containing a statement to execute and a state σ. Values:
41
History
TinyImp Hoare Logic
Dynamic Semantics
We will use big-step operational semantics. What are the sets of evaluable expressions and values here?
Evaluable Expressions: A pair containing a statement to execute and a state σ. Values: The final state that results from executing the statement.
42
History
TinyImp Hoare Logic
Dynamic Semantics
We will use big-step operational semantics. What are the sets of evaluable expressions and values here?
Evaluable Expressions: A pair containing a statement to execute and a state σ. Values: The final state that results from executing the statement.
States
A state is a mutable mapping from variables to their values. We use the following notation:
To read a variable x from the state σ, we write σ(x).
To update an existing variable x to have value v inside the state σ, we write
(σ : x → v).
To extend a state σ with a new, previously undeclared variable x , we write σ · x . In such a state, x has undefined value.
43
History
TinyImp Hoare Logic
Evaluation Rules
We will assume we have defined a relation σ ⊢ e ⇓ v for arithmetic expressions, much like in the previous lecture.
(σ, skip) ⇓ σ
44
History
TinyImp Hoare Logic
Evaluation Rules
We will assume we have defined a relation σ ⊢ e ⇓ v for arithmetic expressions, much like in the previous lecture.
(σ, skip) ⇓ σ (σ1, s1; s2) ⇓
45
History
TinyImp Hoare Logic
Evaluation Rules
We will assume we have defined a relation σ ⊢ e ⇓ v for arithmetic expressions, much like in the previous lecture.
(σ1, s1) ⇓ σ2
(σ, skip) ⇓ σ (σ1, s1; s2) ⇓
46
History
TinyImp Hoare Logic
Evaluation Rules
We will assume we have defined a relation σ ⊢ e ⇓ v for arithmetic expressions, much like in the previous lecture.
(σ1, s1) ⇓ σ2 (σ2, s2) ⇓ σ3 (σ, skip) ⇓ σ (σ1, s1; s2) ⇓
47
History
TinyImp Hoare Logic
Evaluation Rules
We will assume we have defined a relation σ ⊢ e ⇓ v for arithmetic expressions, much like in the previous lecture.
(σ1, s1) ⇓ σ2 (σ2, s2) ⇓ σ3 (σ,skip) ⇓ σ (σ1,s1;s2) ⇓ σ3
48
History
TinyImp Hoare Logic
Evaluation Rules
We will assume we have defined a relation σ ⊢ e ⇓ v for arithmetic expressions, much like in the previous lecture.
(σ,skip) ⇓ σ σ⊢e⇓v
(σ,x := e) ⇓
(σ1, s1) ⇓ σ2 (σ2, s2) ⇓ σ3 (σ1,s1;s2) ⇓ σ3
49
History
TinyImp Hoare Logic
Evaluation Rules
We will assume we have defined a relation σ ⊢ e ⇓ v for arithmetic expressions, much like in the previous lecture.
(σ1, s1) ⇓ σ2 (σ2, s2) ⇓ σ3 (σ,skip) ⇓ σ (σ1,s1;s2) ⇓ σ3
σ⊢e⇓v
(σ,x := e) ⇓ (σ : x → v)
50
History
TinyImp Hoare Logic
Evaluation Rules
We will assume we have defined a relation σ ⊢ e ⇓ v for arithmetic expressions, much like in the previous lecture.
(σ1, s1) ⇓ σ2 (σ2, s2) ⇓ σ3 (σ,skip) ⇓ σ (σ1,s1;s2) ⇓ σ3
σ⊢e⇓v
(σ,x:=e)⇓(σ:x→v) (σ1,varx·s)⇓
51
History
TinyImp Hoare Logic
Evaluation Rules
We will assume we have defined a relation σ ⊢ e ⇓ v for arithmetic expressions, much like in the previous lecture.
(σ1, s1) ⇓ σ2 (σ2, s2) ⇓ σ3 (σ,skip) ⇓ σ (σ1,s1;s2) ⇓ σ3
σ ⊢ e ⇓ v (σ1 · x , s ) ⇓ (σ2 · x ) (σ,x:=e)⇓(σ:x→v) (σ1,varx·s)⇓
52
History
TinyImp Hoare Logic
Evaluation Rules
We will assume we have defined a relation σ ⊢ e ⇓ v for arithmetic expressions, much like in the previous lecture.
(σ1, s1) ⇓ σ2 (σ2, s2) ⇓ σ3 (σ,skip) ⇓ σ (σ1,s1;s2) ⇓ σ3
σ ⊢ e ⇓ v (σ1 · x , s ) ⇓ (σ2 · x ) (σ,x:=e)⇓(σ:x→v) (σ1,varx·s)⇓σ2
53
History
TinyImp Hoare Logic
Evaluation Rules
We will assume we have defined a relation σ ⊢ e ⇓ v for arithmetic expressions, much like in the previous lecture.
(σ1, s1) ⇓ σ2 (σ2, s2) ⇓ σ3 (σ,skip) ⇓ σ (σ1,s1;s2) ⇓ σ3
σ ⊢ e ⇓ v (σ1 · x , s ) ⇓ (σ2 · x ) (σ,x:=e)⇓(σ:x→v) (σ1,varx·s)⇓σ2
(σ1,if e then s1 else s2 fi) ⇓ (σ1,if e then s1 else s2 fi) ⇓
54
History
TinyImp Hoare Logic
Evaluation Rules
We will assume we have defined a relation σ ⊢ e ⇓ v for arithmetic expressions, much like in the previous lecture.
(σ1, s1) ⇓ σ2 (σ2, s2) ⇓ σ3 (σ,skip) ⇓ σ (σ1,s1;s2) ⇓ σ3
σ ⊢ e ⇓ v (σ1 · x , s ) ⇓ (σ2 · x ) (σ,x:=e)⇓(σ:x→v) (σ1,varx·s)⇓σ2
σ1 ⊢ e ⇓ v v ̸= 0
(σ1,if e then s1 else s2 fi) ⇓
(σ1,if e then s1 else s2 fi) ⇓
55
History
TinyImp Hoare Logic
Evaluation Rules
We will assume we have defined a relation σ ⊢ e ⇓ v for arithmetic expressions, much like in the previous lecture.
(σ1, s1) ⇓ σ2 (σ2, s2) ⇓ σ3 (σ,skip) ⇓ σ (σ1,s1;s2) ⇓ σ3
σ ⊢ e ⇓ v (σ1 · x , s ) ⇓ (σ2 · x ) (σ,x:=e)⇓(σ:x→v) (σ1,varx·s)⇓σ2
σ1 ⊢ e ⇓ v v ̸= 0 (σ1,s1) ⇓ σ2 (σ1,if e then s1 else s2 fi) ⇓
(σ1,if e then s1 else s2 fi) ⇓
56
History
TinyImp Hoare Logic
Evaluation Rules
We will assume we have defined a relation σ ⊢ e ⇓ v for arithmetic expressions, much like in the previous lecture.
(σ1, s1) ⇓ σ2 (σ2, s2) ⇓ σ3 (σ,skip) ⇓ σ (σ1,s1;s2) ⇓ σ3
σ ⊢ e ⇓ v (σ1 · x , s ) ⇓ (σ2 · x ) (σ,x:=e)⇓(σ:x→v) (σ1,varx·s)⇓σ2
σ1 ⊢ e ⇓ v v ̸= 0 (σ1,s1) ⇓ σ2 (σ1,if e then s1 else s2 fi) ⇓ σ2
(σ1,if e then s1 else s2 fi) ⇓
57
History
TinyImp Hoare Logic
Evaluation Rules
We will assume we have defined a relation σ ⊢ e ⇓ v for arithmetic expressions, much like in the previous lecture.
(σ1, s1) ⇓ σ2 (σ2, s2) ⇓ σ3 (σ,skip) ⇓ σ (σ1,s1;s2) ⇓ σ3
σ ⊢ e ⇓ v (σ1 · x , s ) ⇓ (σ2 · x ) (σ,x:=e)⇓(σ:x→v) (σ1,varx·s)⇓σ2
σ1 ⊢ e ⇓ v v ̸= 0 (σ1,s1) ⇓ σ2 (σ1,if e then s1 else s2 fi) ⇓ σ2
σ1 ⊢ e ⇓ 0
(σ1,if e then s1 else s2 fi) ⇓
58
History
TinyImp Hoare Logic
Evaluation Rules
We will assume we have defined a relation σ ⊢ e ⇓ v for arithmetic expressions, much like in the previous lecture.
(σ1, s1) ⇓ σ2 (σ2, s2) ⇓ σ3 (σ,skip) ⇓ σ (σ1,s1;s2) ⇓ σ3
σ ⊢ e ⇓ v (σ1 · x , s ) ⇓ (σ2 · x ) (σ,x:=e)⇓(σ:x→v) (σ1,varx·s)⇓σ2
σ1 ⊢ e ⇓ v v ̸= 0 (σ1,s1) ⇓ σ2 (σ1,if e then s1 else s2 fi) ⇓ σ2 σ1 ⊢ e ⇓ 0 (σ1,s2) ⇓ σ2 (σ1,if e then s1 else s2 fi) ⇓ σ2
59
History
TinyImp Hoare Logic
Evaluation Rules
We will assume we have defined a relation σ ⊢ e ⇓ v for arithmetic expressions, much like in the previous lecture.
(σ1, s1) ⇓ σ2 (σ2, s2) ⇓ σ3 (σ,skip) ⇓ σ (σ1,s1;s2) ⇓ σ3
σ ⊢ e ⇓ v (σ1 · x , s ) ⇓ (σ2 · x ) (σ,x:=e)⇓(σ:x→v) (σ1,varx·s)⇓σ2
σ1 ⊢ e ⇓ v v ̸= 0 (σ1,s1) ⇓ σ2 (σ1,if e then s1 else s2 fi) ⇓ σ2 σ1 ⊢ e ⇓ 0 (σ1,s2) ⇓ σ2 (σ1,if e then s1 else s2 fi) ⇓ σ2
60
(σ1,while e do s od) ⇓ (σ1,while e do s od) ⇓
History
TinyImp Hoare Logic
61
Evaluation Rules
We will assume we have defined a relation σ ⊢ e ⇓ v for arithmetic expressions, much like in the previous lecture.
(σ1, s1) ⇓ σ2 (σ2, s2) ⇓ σ3 (σ,skip) ⇓ σ (σ1,s1;s2) ⇓ σ3
σ ⊢ e ⇓ v (σ1 · x , s ) ⇓ (σ2 · x ) (σ,x:=e)⇓(σ:x→v) (σ1,varx·s)⇓σ2
σ1 ⊢ e ⇓ v v ̸= 0 (σ1,s1) ⇓ σ2 (σ1,if e then s1 else s2 fi) ⇓ σ2 σ1 ⊢ e ⇓ 0 (σ1,s2) ⇓ σ2 (σ1,if e then s1 else s2 fi) ⇓ σ2
σ1 ⊢ e ⇓ 0
(σ1,while e do s od) ⇓ (σ1,while e do s od) ⇓
History
TinyImp Hoare Logic
62
Evaluation Rules
We will assume we have defined a relation σ ⊢ e ⇓ v for arithmetic expressions, much like in the previous lecture.
(σ1, s1) ⇓ σ2 (σ2, s2) ⇓ σ3 (σ,skip) ⇓ σ (σ1,s1;s2) ⇓ σ3
σ ⊢ e ⇓ v (σ1 · x , s ) ⇓ (σ2 · x ) (σ,x:=e)⇓(σ:x→v) (σ1,varx·s)⇓σ2
σ1 ⊢ e ⇓ v v ̸= 0 (σ1,s1) ⇓ σ2 (σ1,if e then s1 else s2 fi) ⇓ σ2 σ1 ⊢ e ⇓ 0 (σ1,s2) ⇓ σ2 (σ1,if e then s1 else s2 fi) ⇓ σ2
σ1 ⊢ e ⇓ 0
(σ1,while e do s od) ⇓ σ1 (σ1,while e do s od) ⇓
History
TinyImp Hoare Logic
Evaluation Rules
We will assume we have defined a relation σ ⊢ e ⇓ v for arithmetic expressions, much like in the previous lecture.
(σ1, s1) ⇓ σ2 (σ2, s2) ⇓ σ3 (σ,skip) ⇓ σ (σ1,s1;s2) ⇓ σ3
σ ⊢ e ⇓ v (σ1 · x , s ) ⇓ (σ2 · x ) (σ,x:=e)⇓(σ:x→v) (σ1,varx·s)⇓σ2
σ1 ⊢ e ⇓ v v ̸= 0 (σ1,s1) ⇓ σ2 (σ1,if e then s1 else s2 fi) ⇓ σ2 σ1 ⊢ e ⇓ 0 (σ1,s2) ⇓ σ2 (σ1,if e then s1 else s2 fi) ⇓ σ2
σ1⊢e⇓v v̸=0 (σ1,while e do s od) ⇓ σ1 (σ1,while e do s od) ⇓
σ1 ⊢ e ⇓ 0
63
History
TinyImp Hoare Logic
Evaluation Rules
We will assume we have defined a relation σ ⊢ e ⇓ v for arithmetic expressions, much like in the previous lecture.
(σ1, s1) ⇓ σ2 (σ2, s2) ⇓ σ3 (σ,skip) ⇓ σ (σ1,s1;s2) ⇓ σ3
σ ⊢ e ⇓ v (σ1 · x , s ) ⇓ (σ2 · x ) (σ,x:=e)⇓(σ:x→v) (σ1,varx·s)⇓σ2
σ1 ⊢ e ⇓ v v ̸= 0 (σ1,s1) ⇓ σ2 (σ1,if e then s1 else s2 fi) ⇓ σ2 σ1 ⊢ e ⇓ 0 (σ1,s2) ⇓ σ2 (σ1,if e then s1 else s2 fi) ⇓ σ2
σ1⊢e⇓v v̸=0 σ1 ⊢ e ⇓ 0 (σ1,s) ⇓ σ2
64
(σ1,while e do s od) ⇓ σ1 (σ1,while e do s od) ⇓
History
TinyImp Hoare Logic
Evaluation Rules
We will assume we have defined a relation σ ⊢ e ⇓ v for arithmetic expressions, much like in the previous lecture.
(σ1, s1) ⇓ σ2 (σ2, s2) ⇓ σ3 (σ,skip) ⇓ σ (σ1,s1;s2) ⇓ σ3
σ ⊢ e ⇓ v (σ1 · x , s ) ⇓ (σ2 · x ) (σ,x:=e)⇓(σ:x→v) (σ1,varx·s)⇓σ2
σ1 ⊢ e ⇓ v v ̸= 0 (σ1,s1) ⇓ σ2 (σ1,if e then s1 else s2 fi) ⇓ σ2 σ1 ⊢ e ⇓ 0 (σ1,s2) ⇓ σ2 (σ1,if e then s1 else s2 fi) ⇓ σ2
σ1⊢e⇓v v̸=0
σ1 ⊢ e ⇓ 0 (σ1,s) ⇓ σ2 (σ2,while e do s od) ⇓ σ3
65
(σ1,while e do s od) ⇓ σ1 (σ1,while e do s od) ⇓
History
TinyImp Hoare Logic
Evaluation Rules
We will assume we have defined a relation σ ⊢ e ⇓ v for arithmetic expressions, much like in the previous lecture.
(σ1, s1) ⇓ σ2 (σ2, s2) ⇓ σ3 (σ,skip) ⇓ σ (σ1,s1;s2) ⇓ σ3
σ ⊢ e ⇓ v (σ1 · x , s ) ⇓ (σ2 · x ) (σ,x:=e)⇓(σ:x→v) (σ1,varx·s)⇓σ2
σ1 ⊢ e ⇓ v v ̸= 0 (σ1,s1) ⇓ σ2 (σ1,if e then s1 else s2 fi) ⇓ σ2 σ1 ⊢ e ⇓ 0 (σ1,s2) ⇓ σ2 (σ1,if e then s1 else s2 fi) ⇓ σ2
σ1⊢e⇓v v̸=0
σ1 ⊢ e ⇓ 0 (σ1,s) ⇓ σ2 (σ2,while e do s od) ⇓ σ3
66
(σ1,while e do s od) ⇓ σ1 (σ1,while e do s od) ⇓ σ3
History
TinyImp Hoare Logic
Hoare Logic
To give you a taste of axiomatic semantics, and also how formal verification works, we are going to define what’s called a Hoare Logic for TinyImp to allow us to prove properties of our program.
We write a Hoare triple judgement as:
{φ} s {ψ}
Where φ and ψ are logical formulae about state variables, called assertions, and s is a statement. This triple states that if the statement s successfully evaluates from a starting state satisfying the precondition φ, then the result state will satisfy the postcondition ψ:
φ(σ)∧(σ,s)⇓σ′ ⇒ψ(σ′)
67
History
TinyImp
Hoare Logic
To prove a Hoare triple like:
Proving Hoare Triples
{True}
var i · var m ·
i := 0;
m := 1;
while i < N do
i := i + 1;
m := m × i od
{m = N!}
It is undesirable to look at the operational semantics derivations of this whole program to compute what the possible final states are for a given input state. Instead we shall define a set of rules to prove Hoare triples directly (called a proof calculus).
68
History
TinyImp
Hoare Logic
(σ, skip) ⇓ σ
(σ1, s1) ⇓ σ2 (σ2, s2) ⇓ σ3
(σ1, s1; s2) ⇓ σ3
σ⊢e⇓v
(σ,x := e) ⇓ (σ : x → v)
Hoare Rules
{φ} skip
69
History
TinyImp
Hoare Logic
(σ, skip) ⇓ σ
(σ1, s1) ⇓ σ2 (σ2, s2) ⇓ σ3
(σ1, s1; s2) ⇓ σ3
σ⊢e⇓v
(σ,x := e) ⇓ (σ : x → v)
Hoare Rules
{φ} skip {φ}
70
History
TinyImp
Hoare Logic
(σ, skip) ⇓ σ
(σ1, s1) ⇓ σ2 (σ2, s2) ⇓ σ3
(σ1, s1; s2) ⇓ σ3
σ⊢e⇓v
(σ,x := e) ⇓ (σ : x → v)
Hoare Rules
{φ} skip {φ}
{φ} s1; s2
71
History
TinyImp
Hoare Logic
(σ, skip) ⇓ σ
(σ1,s1) ⇓ σ2 (σ2,s2) ⇓ σ3
(σ1,s1;s2)⇓σ3
σ⊢e⇓v
(σ,x := e) ⇓ (σ : x → v)
Hoare Rules
{φ} skip {φ}
{φ} s1 {α} {α} s2 {ψ} {φ}s1;s2 {ψ}
72
History
TinyImp
Hoare Logic
(σ, skip) ⇓ σ
(σ1,s1) ⇓ σ2 (σ2,s2) ⇓ σ3
(σ1,s1;s2)⇓σ3
σ⊢e⇓v
(σ,x := e) ⇓ (σ : x → v)
Hoare Rules
{φ} skip {φ}
{φ} s1 {α} {α} s2 {ψ}
{φ}s1;s2 {ψ}
x := e {φ}
73
History
TinyImp
Hoare Logic
(σ, skip) ⇓ σ
(σ1,s1) ⇓ σ2 (σ2,s2) ⇓ σ3
(σ1,s1;s2)⇓σ3 σ⊢e⇓v
Hoare Rules
{φ} skip {φ}
{φ} s1 {α} {α} s2 {ψ}
{φ}s1;s2 {ψ} {φ[x := e]} x := e {φ}
(σ,x := e) ⇓ (σ : x → v)
Continuing on, we can get rules for if, and while with a loop invariant:
{φ}ife thens1 elses2 fi{ψ} {φ}whilee dos od
74
History
TinyImp
Hoare Logic
(σ, skip) ⇓ σ
(σ1,s1) ⇓ σ2 (σ2,s2) ⇓ σ3
(σ1,s1;s2)⇓σ3 σ⊢e⇓v
(σ,x := e) ⇓ (σ : x → v)
Hoare Rules
{φ} skip {φ}
{φ} s1 {α} {α} s2 {ψ}
{φ}s1;s2 {ψ} {φ[x := e]} x := e {φ}
Continuing on, we can get rules for if, and while with a loop invariant:
{φ∧e}s1 {ψ}
{φ}ife thens1 elses2 fi{ψ} {φ}whilee dos od
75
History
TinyImp
Hoare Logic
(σ, skip) ⇓ σ
(σ1,s1) ⇓ σ2 (σ2,s2) ⇓ σ3
(σ1,s1;s2)⇓σ3 σ⊢e⇓v
(σ,x := e) ⇓ (σ : x → v)
Hoare Rules
{φ} skip {φ}
{φ} s1 {α} {α} s2 {ψ}
{φ}s1;s2 {ψ} {φ[x := e]} x := e {φ}
Continuing on, we can get rules for if, and while with a loop invariant:
{φ∧e} s1 {ψ} {φ∧¬e} s2 {ψ}
{φ}ife thens1 elses2 fi{ψ} {φ}whilee dos od
76
History
TinyImp
Hoare Logic
(σ, skip) ⇓ σ
(σ1,s1) ⇓ σ2 (σ2,s2) ⇓ σ3
(σ1,s1;s2)⇓σ3 σ⊢e⇓v
(σ,x := e) ⇓ (σ : x → v)
Hoare Rules
{φ} skip {φ}
{φ} s1 {α} {α} s2 {ψ}
{φ}s1;s2 {ψ} {φ[x := e]} x := e {φ}
Continuing on, we can get rules for if, and while with a loop invariant:
{φ∧e} s1 {ψ} {φ∧¬e} s2 {ψ} {φ∧e} s {φ} {φ}ife thens1 elses2 fi{ψ} {φ}whilee dos od
77
History
TinyImp
Hoare Logic
(σ, skip) ⇓ σ
(σ1,s1) ⇓ σ2 (σ2,s2) ⇓ σ3
(σ1,s1;s2)⇓σ3 σ⊢e⇓v
(σ,x := e) ⇓ (σ : x → v)
Hoare Rules
{φ} skip {φ}
{φ} s1 {α} {α} s2 {ψ}
{φ}s1;s2 {ψ} {φ[x := e]} x := e {φ}
Continuing on, we can get rules for if, and while with a loop invariant:
{φ∧e} s1 {ψ} {φ∧¬e} s2 {ψ} {φ∧e} s {φ} {φ}ife thens1 elses2 fi{ψ} {φ}whilee dos od{φ∧¬e}
78
History
TinyImp Hoare Logic
Consequence
There is one more rule, called the rule of consequence, that we need to insert ordinary logical reasoning into our Hoare logic proofs:
φ ⇒ α {α} s {β} β ⇒ ψ {φ} s {ψ}
79
History
TinyImp Hoare Logic
Consequence
There is one more rule, called the rule of consequence, that we need to insert ordinary logical reasoning into our Hoare logic proofs:
φ ⇒ α {α} s {β} β ⇒ ψ {φ} s {ψ}
This is the only rule that is not directed entirely by syntax. This means a Hoare logic proof need not look like a derivation tree. Instead we can sprinkle assertions through our program and specially note uses of the consequence rule.
80
History
TinyImp
Hoare Logic
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{True}
var i · var m ·
i := 0; m := 1;
while i < N do i := i + 1;
m := m × i
od
{m = N!}
{φ∧e} s1 {ψ} {φ∧¬e} s2 {ψ} {φ}ife thens1 elses2 fi{ψ}
{φ[x := e]} x := e {φ} {φ ∧ e} s {φ}
{φ} while e do s od {φ∧¬e} {φ} s1 {α} {α} s2 {ψ}
{φ}s1;s2 {ψ}
φ ⇒ α {α} s {β} β ⇒ ψ {φ} s {ψ}
81
History
TinyImp
Hoare Logic
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{True}
var i · var m ·
i := 0; m := 1;
while i < N do i := i + 1;
m := m × i
od{m=i!∧i =N} {m = N!}
{φ∧e} s1 {ψ} {φ∧¬e} s2 {ψ} {φ}ife thens1 elses2 fi{ψ}
{φ[x := e]} x := e {φ} {φ ∧ e} s {φ}
{φ} while e do s od {φ∧¬e} {φ} s1 {α} {α} s2 {ψ}
{φ}s1;s2 {ψ}
φ ⇒ α {α} s {β} β ⇒ ψ {φ} s {ψ}
82
History
TinyImp
Hoare Logic
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{True}
var i · var m ·
i := 0; m := 1;
{m = i!}
while i < N do
i := i + 1;
m := m × i
od{m=i!∧i =N} {m = N!}
{φ∧e} s1 {ψ} {φ∧¬e} s2 {ψ} {φ}ife thens1 elses2 fi{ψ}
{φ[x := e]} x := e {φ} {φ ∧ e} s {φ}
{φ} while e do s od {φ∧¬e} {φ} s1 {α} {α} s2 {ψ}
{φ}s1;s2 {ψ}
φ ⇒ α {α} s {β} β ⇒ ψ {φ} s {ψ}
83
History
TinyImp
Hoare Logic
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{True}
var i · var m ·
i := 0; m := 1;
{m = i!}
while i < N do
i := i + 1;
m := m × i
{m = i!} od{m=i!∧i =N} {m = N!}
{φ∧e} s1 {ψ} {φ∧¬e} s2 {ψ} {φ}ife thens1 elses2 fi{ψ}
{φ[x := e]} x := e {φ} {φ ∧ e} s {φ}
{φ} while e do s od {φ∧¬e}
{φ} s1 {α} {α} s2 {ψ} {φ}s1;s2 {ψ}
φ ⇒ α
{α} s {β} {φ} s {ψ}
β ⇒ ψ
84
History
TinyImp
Hoare Logic
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{True}
var i · var m ·
i := 0; m := 1;
{m = i!}
while i < N do {m = i! ∧ i < N}
i := i + 1;
m := m × i
{m = i!} od{m=i!∧i =N} {m = N!}
{φ∧e} s1 {ψ} {φ∧¬e} s2 {ψ} {φ}ife thens1 elses2 fi{ψ}
{φ[x := e]} x := e {φ} {φ ∧ e} s {φ}
{φ} while e do s od {φ∧¬e}
{φ} s1 {α} {α} s2 {ψ} {φ}s1;s2 {ψ}
φ ⇒ α
{α} s {β} {φ} s {ψ}
β ⇒ ψ
85
History
TinyImp
Hoare Logic
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{True}
var i · var m ·
i := 0; m := 1;
{m = i!}
while i < N do {m = i! ∧ i < N}
i := i + 1; {m × i = i!} m := m × i {m = i!}
od{m=i!∧i =N} {m = N!}
{φ∧e} s1 {ψ} {φ∧¬e} s2 {ψ} {φ}ife thens1 elses2 fi{ψ}
{φ[x := e]} x := e {φ} {φ ∧ e} s {φ}
{φ} while e do s od {φ∧¬e}
{φ} s1 {α} {α} s2 {ψ} {φ}s1;s2 {ψ}
φ ⇒ α
{α} s {β} {φ} s {ψ}
β ⇒ ψ
86
History
TinyImp
Hoare Logic
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{True}
var i · var m ·
i := 0; m := 1;
{m = i!}
while i < N do {m = i! ∧ i < N}
{m × (i + 1) = (i + 1)!} i := i + 1;
{m × i = i!}
m := m × i
{m = i!} od{m=i!∧i =N} {m = N!}
{φ∧e} s1 {ψ} {φ∧¬e} s2 {ψ} {φ}ife thens1 elses2 fi{ψ}
{φ[x := e]} x := e {φ} {φ ∧ e} s {φ}
{φ} while e do s od {φ∧¬e}
{φ} s1 {α} {α} s2 {ψ} {φ}s1;s2 {ψ}
φ ⇒ α
{α} s {β} {φ} s {ψ}
β ⇒ ψ
87
History
TinyImp
Hoare Logic
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{True}
var i · var m ·
i := 0; m := 1;
{m = i!}
while i < N do {m = i! ∧ i < N}
{m × (i + 1) = (i + 1)!} i := i + 1;
{m × i = i!}
m := m × i
{m = i!} od{m=i!∧i =N} {m = N!}
{φ∧e} s1 {ψ} {φ∧¬e} s2 {ψ} {φ}ife thens1 elses2 fi{ψ}
{φ[x := e]} x := e {φ} {φ ∧ e} s {φ}
{φ} while e do s od {φ∧¬e}
{φ} s1 {α} {α} s2 {ψ} {φ}s1;s2 {ψ}
φ ⇒ α
{α} s {β} {φ} s {ψ}
β ⇒ ψ
note: (i +1)! = i!×(i +1)
88
History
TinyImp
Hoare Logic
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{True}
var i · var m ·
i := 0;
m := 1;{m = i!}
{m = i!}
while i < N do {m = i! ∧ i < N}
{m × (i + 1) = (i + 1)!} i := i + 1;
{m × i = i!}
m := m × i
{m = i!} od{m=i!∧i =N} {m = N!}
{φ∧e} s1 {ψ} {φ∧¬e} s2 {ψ} {φ}ife thens1 elses2 fi{ψ}
{φ[x := e]} x := e {φ} {φ ∧ e} s {φ}
{φ} while e do s od {φ∧¬e}
{φ} s1 {α} {α} s2 {ψ} {φ}s1;s2 {ψ}
φ ⇒ α
{α} s {β} {φ} s {ψ}
β ⇒ ψ
note: (i +1)! = i!×(i +1)
89
History
TinyImp
Hoare Logic
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{True}
var i · var m ·
i := 0;
{1 = i!}m := 1;{m = i!}
{m = i!}
while i < N do {m = i! ∧ i < N}
{m × (i + 1) = (i + 1)!} i := i + 1;
{m × i = i!}
m := m × i
{m = i!} od{m=i!∧i =N} {m = N!}
{φ∧e} s1 {ψ} {φ∧¬e} s2 {ψ} {φ}ife thens1 elses2 fi{ψ}
{φ[x := e]} x := e {φ} {φ ∧ e} s {φ}
{φ} while e do s od {φ∧¬e}
{φ} s1 {α} {α} s2 {ψ} {φ}s1;s2 {ψ}
φ ⇒ α
{α} s {β} {φ} s {ψ}
β ⇒ ψ
note: (i +1)! = i!×(i +1)
90
History
TinyImp
Hoare Logic
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{True}
var i · var m ·
i := 0;{1 = i!} {1 = i!}m := 1;{m = i!}
{m = i!}
while i < N do {m = i! ∧ i < N}
{m × (i + 1) = (i + 1)!} i := i + 1;
{m × i = i!}
m := m × i
{m = i!} od{m=i!∧i =N} {m = N!}
{φ∧e} s1 {ψ} {φ∧¬e} s2 {ψ} {φ}ife thens1 elses2 fi{ψ}
{φ[x := e]} x := e {φ} {φ ∧ e} s {φ}
{φ} while e do s od {φ∧¬e}
{φ} s1 {α} {α} s2 {ψ} {φ}s1;s2 {ψ}
φ ⇒ α
{α} s {β} {φ} s {ψ}
β ⇒ ψ
note: (i +1)! = i!×(i +1)
91
History
TinyImp
Hoare Logic
Factorial Example
Let’s verify the Factorial program using our Hoare rules:
{True}
var i · var m ·
{1 = 0!}i := 0;{1 = i!}
{1 = i!}m := 1;{m = i!}
{m = i!}
while i < N do {m = i! ∧ i < N}
{m × (i + 1) = (i + 1)!} i := i + 1;
{m × i = i!}
m := m × i
{m = i!} od{m=i!∧i =N} {m = N!}
{φ∧e} s1 {ψ} {φ∧¬e} s2 {ψ} {φ}ife thens1 elses2 fi{ψ}
{φ[x := e]} x := e {φ} {φ ∧ e} s {φ}
{φ} while e do s od {φ∧¬e}
{φ} s1 {α} {α} s2 {ψ} {φ}s1;s2 {ψ}
φ ⇒ α
{α} s {β} {φ} s {ψ}
β ⇒ ψ
note: (i +1)! = i!×(i +1)
92