Program Correctness: Jorge A. Pérez
Program Correctness: Jorge A. Pérez
Program Correctness: Jorge A. Pérez
Lecture 1
Jorge A. Pérez
(based on slides by Arnold Meijster)
February 6, 2023
Overview
Mathematical Background
Hoare Logic
Triples
Assignments
Weakening and Strengthening
Sequential Composition and Conditionals
Examples of Annotations
Assignments
Conditionals
Exercise 5.6
Summary of Background
2 / 60
This Course
fP g S fQ g
S is a program statement (or command)
P and Q are logical formulas: precondition and postcondition
I Intuitively, a contract:
If we can ensure property P holds before executing S , then we
are guaranteed that property Q holds after the execution ends.
I Our goal is to prove that fP g S fQ g is valid.
Starting from P and Q, we deduce S by applying rules.
Actually, we discover S based on P and Q.
3 / 60
Outline
Mathematical Background
Hoare Logic
Triples
Assignments
Weakening and Strengthening
Sequential Composition and Conditionals
Examples of Annotations
Assignments
Conditionals
Exercise 5.6
Summary of Background
4 / 60
Background
We don’t fully repeat this content here. See at the end for a recap.
5 / 60
Identifiers
I constants:
1 ;:::; 2; 1; 0; 1; 2; : : : ; 1;
I variables
i ; j ; k ; m ; n ; p; q ; v ; w ; x ; y ; z
I specification constants (logical variables):
M;V;X;Y ;Z
I arrays:
a; b
6 / 60
Types as Sets of Values
7 / 60
Formulas / Conditions
Examples:
I atomic proposition:
x +3 > a [0]2 X =m +n
I (compound) proposition:
( n = 2 ^ m 0) ) m n y
I predicate:
8x (x 0 ) 9y (y 0 ^ x + y = 0))
8 / 60
Declarations
9 / 60
Outline
Mathematical Background
Hoare Logic
Triples
Assignments
Weakening and Strengthening
Sequential Composition and Conditionals
Examples of Annotations
Assignments
Conditionals
Exercise 5.6
Summary of Background
10 / 60
Program States
domain of xi .
I A program’s execution depends on its current state.
I The state space is the set of all possible states of a program.
I We often talk about commands, rather than programs.
11 / 60
Program Correctness
12 / 60
Program Correctness
More precisely:
I Let S be a command with declared variables x0 ; : : : ; xn 1 .
I S is specified by a precondition P and a postcondition Q.
I P describes the state before execution of S
I Q describes the state after execution of S
I Formally, P and Q are formulas whose free variables are
x0 ; : : : ; xn 1 and specification constants X ; Y ; : : :.
12 / 60
A Small Programming Language
Syntax Description
skip Does nothing
x := E Store E into the variable x
S; T Run S followed by T
if B then S else T end If B is true then run S else run T
while B do S end As long as B is true then run S
14 / 60
Two Simple Programs
Program A: Program B:
y := 1;
y := x ;
z := 0;
while (2 y ) do
while (z 6= x ) do
y := y 2
z := z + 1;
y := y z
end
end
15 / 60
Two Simple Programs
Program A: Program B:
y := 1;
y := x ;
z := 0;
while (2 y ) do
while (z 6= x ) do
y := y 2
z := z + 1;
y := y z
end
end
15 / 60
Triples
fP g S fQ g
Intuitive reading:
I “If we execute S in any state in which (property) P holds,
then S will terminate in a state in which (property) Q holds”
16 / 60
Triples
fP g S fQ g
Intuitive reading:
I “If we execute S in any state in which (property) P holds,
then S will terminate in a state in which (property) Q holds”
16 / 60
Valid Tuples, Informally
Given the intended reading for the tuple fP g S fQ g
“If we execute S in any state in which (property) P holds,
then S will terminate in a state in which (property) Q holds”
we wish to identify valid tuples only.
17 / 60
Valid Tuples, Informally
Given the intended reading for the tuple fP g S fQ g
“If we execute S in any state in which (property) P holds,
then S will terminate in a state in which (property) Q holds”
we wish to identify valid tuples only.
Let’s start with intuitions — valid or invalid?
I fi = 0g i := i + 1 fi = 1g
17 / 60
Valid Tuples, Informally
Given the intended reading for the tuple fP g S fQ g
“If we execute S in any state in which (property) P holds,
then S will terminate in a state in which (property) Q holds”
we wish to identify valid tuples only.
Let’s start with intuitions — valid or invalid?
I fi = 0g i := i + 1 fi = 1g Valid
17 / 60
Valid Tuples, Informally
Given the intended reading for the tuple fP g S fQ g
“If we execute S in any state in which (property) P holds,
then S will terminate in a state in which (property) Q holds”
we wish to identify valid tuples only.
Let’s start with intuitions — valid or invalid?
I fi = 0g i := i + 1 fi = 1g Valid
I fi = 1g i := i + 1 fi = 0g
17 / 60
Valid Tuples, Informally
Given the intended reading for the tuple fP g S fQ g
“If we execute S in any state in which (property) P holds,
then S will terminate in a state in which (property) Q holds”
we wish to identify valid tuples only.
Let’s start with intuitions — valid or invalid?
I fi = 0g i := i + 1 fi = 1g Valid
I fi = 1g i := i + 1 fi = 0g Invalid
17 / 60
Valid Tuples, Informally
Given the intended reading for the tuple fP g S fQ g
“If we execute S in any state in which (property) P holds,
then S will terminate in a state in which (property) Q holds”
we wish to identify valid tuples only.
Let’s start with intuitions — valid or invalid?
I fi = 0g i := i + 1 fi = 1g Valid
I fi = 1g i := i + 1 fi = 0g Invalid
I ftrueg i := 1 fi = 1g
17 / 60
Valid Tuples, Informally
Given the intended reading for the tuple fP g S fQ g
“If we execute S in any state in which (property) P holds,
then S will terminate in a state in which (property) Q holds”
we wish to identify valid tuples only.
Let’s start with intuitions — valid or invalid?
I fi = 0g i := i + 1 fi = 1g Valid
I fi = 1g i := i + 1 fi = 0g Invalid
I ftrueg i := 1 fi = 1g Valid
17 / 60
Valid Tuples, Informally
Given the intended reading for the tuple fP g S fQ g
“If we execute S in any state in which (property) P holds,
then S will terminate in a state in which (property) Q holds”
we wish to identify valid tuples only.
Let’s start with intuitions — valid or invalid?
I fi = 0g i := i + 1 fi = 1g Valid
I fi = 1g i := i + 1 fi = 0g Invalid
I ftrueg i := 1 fi = 1g Valid
I fi + j = 0g i := i + 1; j := j 1; fi + j = 0g
17 / 60
Valid Tuples, Informally
Given the intended reading for the tuple fP g S fQ g
“If we execute S in any state in which (property) P holds,
then S will terminate in a state in which (property) Q holds”
we wish to identify valid tuples only.
Let’s start with intuitions — valid or invalid?
I fi = 0g i := i + 1 fi = 1g Valid
I fi = 1g i := i + 1 fi = 0g Invalid
I ftrueg i := 1 fi = 1g Valid
I fi + j = 0g i := i + 1; j := j 1; fi + j = 0g Valid
17 / 60
Valid Tuples, Informally
Given the intended reading for the tuple fP g S fQ g
“If we execute S in any state in which (property) P holds,
then S will terminate in a state in which (property) Q holds”
we wish to identify valid tuples only.
Let’s start with intuitions — valid or invalid?
I fi = 0g i := i + 1 fi = 1g Valid
I fi = 1g i := i + 1 fi = 0g Invalid
I ftrueg i := 1 fi = 1g Valid
I fi + j = 0g i := i + 1; j := j 1; fi + j = 0g Valid
I fi + j 6= 0g i := i + 1; j := j 1; fi + j = 0g
17 / 60
Valid Tuples, Informally
Given the intended reading for the tuple fP g S fQ g
“If we execute S in any state in which (property) P holds,
then S will terminate in a state in which (property) Q holds”
we wish to identify valid tuples only.
Let’s start with intuitions — valid or invalid?
I fi = 0g i := i + 1 fi = 1g Valid
I fi = 1g i := i + 1 fi = 0g Invalid
I ftrueg i := 1 fi = 1g Valid
I fi + j = 0g i := i + 1; j := j 1; fi + j = 0g Valid
I fi + j 6= 0g i := i + 1; j := j 1; fi + j = 0g Invalid
17 / 60
Valid Tuples, Informally
Given the intended reading for the tuple fP g S fQ g
“If we execute S in any state in which (property) P holds,
then S will terminate in a state in which (property) Q holds”
we wish to identify valid tuples only.
Let’s start with intuitions — valid or invalid?
I fi = 0g i := i + 1 fi = 1g Valid
I fi = 1g i := i + 1 fi = 0g Invalid
I ftrueg i := 1 fi = 1g Valid
I fi + j = 0g i := i + 1; j := j 1; fi + j = 0g Valid
I fi + j 6= 0g i := i + 1; j := j 1; fi + j = 0g Invalid
I fi = 1g i := 0 ftrueg
17 / 60
Valid Tuples, Informally
Given the intended reading for the tuple fP g S fQ g
“If we execute S in any state in which (property) P holds,
then S will terminate in a state in which (property) Q holds”
we wish to identify valid tuples only.
Let’s start with intuitions — valid or invalid?
I fi = 0g i := i + 1 fi = 1g Valid
I fi = 1g i := i + 1 fi = 0g Invalid
I ftrueg i := 1 fi = 1g Valid
I fi + j = 0g i := i + 1; j := j 1; fi + j = 0g Valid
I fi + j 6= 0g i := i + 1; j := j 1; fi + j = 0g Invalid
I fi = 1g i := 0 ftrueg Valid
17 / 60
Valid Tuples, Informally
Given the intended reading for the tuple fP g S fQ g
“If we execute S in any state in which (property) P holds,
then S will terminate in a state in which (property) Q holds”
we wish to identify valid tuples only.
Let’s start with intuitions — valid or invalid?
I fi = 0g i := i + 1 fi = 1g Valid
I fi = 1g i := i + 1 fi = 0g Invalid
I ftrueg i := 1 fi = 1g Valid
I fi + j = 0g i := i + 1; j := j 1; fi + j = 0g Valid
I fi + j 6= 0g i := i + 1; j := j 1; fi + j = 0g Invalid
I fi = 1g i := 0 ftrueg Valid
I ffalseg i := 1 fi = 0g
17 / 60
Valid Tuples, Informally
Given the intended reading for the tuple fP g S fQ g
“If we execute S in any state in which (property) P holds,
then S will terminate in a state in which (property) Q holds”
we wish to identify valid tuples only.
Let’s start with intuitions — valid or invalid?
I fi = 0g i := i + 1 fi = 1g Valid
I fi = 1g i := i + 1 fi = 0g Invalid
I ftrueg i := 1 fi = 1g Valid
I fi + j = 0g i := i + 1; j := j 1; fi + j = 0g Valid
I fi + j 6= 0g i := i + 1; j := j 1; fi + j = 0g Invalid
I fi = 1g i := 0 ftrueg Valid
I ffalseg i := 1 fi = 0g Vacuously valid
17 / 60
Valid Tuples, Informally
Given the intended reading for the tuple fP g S fQ g
“If we execute S in any state in which (property) P holds,
then S will terminate in a state in which (property) Q holds”
we wish to identify valid tuples only.
Let’s start with intuitions — valid or invalid?
I fi = 0g i := i + 1 fi = 1g Valid
I fi = 1g i := i + 1 fi = 0g Invalid
I ftrueg i := 1 fi = 1g Valid
I fi + j = 0g i := i + 1; j := j 1; fi + j = 0g Valid
I fi + j 6= 0g i := i + 1; j := j 1; fi + j = 0g Invalid
I fi = 1g i := 0 ftrueg Valid
I ffalseg i := 1 fi = 0g Vacuously valid
I fi = 0g i := 1 ffalseg
17 / 60
Valid Tuples, Informally
Given the intended reading for the tuple fP g S fQ g
“If we execute S in any state in which (property) P holds,
then S will terminate in a state in which (property) Q holds”
we wish to identify valid tuples only.
Let’s start with intuitions — valid or invalid?
I fi = 0g i := i + 1 fi = 1g Valid
I fi = 1g i := i + 1 fi = 0g Invalid
I ftrueg i := 1 fi = 1g Valid
I fi + j = 0g i := i + 1; j := j 1; fi + j = 0g Valid
I fi + j 6= 0g i := i + 1; j := j 1; fi + j = 0g Invalid
I fi = 1g i := 0 ftrueg Valid
I ffalseg i := 1 fi = 0g Vacuously valid
I fi = 0g i := 1 ffalseg Invalid: One can’t end in a false state
17 / 60
Valid Tuples, Informally
Given the intended reading for the tuple fP g S fQ g
“If we execute S in any state in which (property) P holds,
then S will terminate in a state in which (property) Q holds”
we wish to identify valid tuples only.
Let’s start with intuitions — valid or invalid?
I fi = 0g i := i + 1 fi = 1g Valid
I fi = 1g i := i + 1 fi = 0g Invalid
I ftrueg i := 1 fi = 1g Valid
I fi + j = 0g i := i + 1; j := j 1; fi + j = 0g Valid
I fi + j 6= 0g i := i + 1; j := j 1; fi + j = 0g Invalid
I fi = 1g i := 0 ftrueg Valid
I ffalseg i := 1 fi = 0g Vacuously valid
I fi = 0g i := 1 ffalseg Invalid: One can’t end in a false state
Warning! Abuse of notation when using variable i !
17 / 60
Biregular Specifications
Consider a specification
fP g S fQ g
I It is pre-regular if P is independent of the initial values of its
variables (not the constants!)
I It is post-regular if the Q is of the form
18 / 60
An Informal Specification
Given:
I an array a [0::n ) of real values
I a value w which is present in the array
19 / 60
A Formal Specification (1/4)
An initial pre/post-condition:
P : 9i 2 [0 n ) : a [i ] = w
::
Q : a [x ] = w ^ 8i 2 [0 n ) : (a [i ] = w ) x i )
::
20 / 60
A Formal Specification (2/4)
P :X 2 [0 n ) ^ a [X ] = w ^ 8i 2 [0 n ) : (a [i ] = w ) X i )
:: ::
Q :x =X
P can be expressed more compactly:
P : Min fi j 0 i < n ^ a [i ] = w g = X 1
<
21 / 60
A Formal Specification (3/4)
So, the complete specification is:
Equivalently:
var x : N;
fP : trueg
S
f Q : x 2 = 5g
var x : Z;
fP : X 2 = 25g
S
fQ : x = X g
24 / 60
Outline
Mathematical Background
Hoare Logic
Triples
Assignments
Weakening and Strengthening
Sequential Composition and Conditionals
Examples of Annotations
Assignments
Conditionals
Exercise 5.6
Summary of Background
25 / 60
Hoare Logic
26 / 60
Hoare Logic
26 / 60
Rule for skip
fP g skip fP g
I No premises: this is an axiom.
I After running skip in any state in which P holds, we reach a
state in which P holds (actually, we remain in the same state)
27 / 60
A Rule for Assignment?
We shall be looking for another axiom. For the moment:
fP g x := E fQ g
What should P and Q be?
28 / 60
A Rule for Assignment?
We shall be looking for another axiom. For the moment:
fP g x := E fQ g
What should P and Q be? Some guiding intuitions:
I They are related, but cannot be equal.
I After the assignment, Q is a property that depends on x .
We could write Q (x ) to make this dependency explicit.
I What about Q prior to the assignment?
At that point, Q does not depend on x , but on the expression E .
We could write Q (E ) to make this explicit.
28 / 60
A Rule for Assignment?
We shall be looking for another axiom. For the moment:
fP g x := E fQ g
What should P and Q be? Some guiding intuitions:
I They are related, but cannot be equal.
I After the assignment, Q is a property that depends on x .
We could write Q (x ) to make this dependency explicit.
I What about Q prior to the assignment?
At that point, Q does not depend on x , but on the expression E .
We could write Q (E ) to make this explicit.
fQ (E )g x := E fQ (x )g
but we prefer something more precise than ‘Q (E )’ and ‘Q (x )’. 28 / 60
Rule for Assignment
29 / 60
Rule for Assignment
f[E x ]P g x := E fP g
=
29 / 60
Rule for Assignment
f[E x ]P g x := E fP g
=
30 / 60
Rule for Assignment
f[E x ]P g x := E fP g
=
30 / 60
Rule for Assignment
f[E x ]P g x := E fP g
=
30 / 60
Rules for Pre- and Postconditions (1/2)
Weaker? Stronger?
I If P ) P 0 but not P 0 ) P , then
P 0 is weaker than P (and P is stronger than P 0 ).
I Example:
(x > 1) is weaker than (x > 0), because (x > 0) ) (x > 1).
I The weakest possible predicate is true,
because P ) true, for any P .
I The strongest possible predicate is false
31 / 60
Rules for Pre- and Postconditions (2/2)
32 / 60
Rules for Pre- and Postconditions (2/2)
32 / 60
Example: Strengthening Precondition
33 / 60
Example: Strengthening Precondition
33 / 60
Linear Annotated Proofs
Rather than derivations like
fx = 5g
(* logic to “prepare” the assignment *)
f[x + 1 x ](x = 6)g
=
x := x + 1
fx = 6g
34 / 60
Linear Annotated Proofs
Rather than derivations like
fx = 5g
(* logic to “prepare” the assignment *)
f[x + 1 x ](x = 6)g
=
x := x + 1
fx = 6g
I If fP g and fQ g appear after each other without a command,
then P ) Q. A comment must justify this implication.
I Indentation highlights commands from conditions.
We use colors to further improve readability.
34 / 60
Rule for Sequential Composition
fP g S fQ g fQ g T fRg
fP g S ; T fRg
I Reasoning is modular: to verify the composite command
‘S ; T ’, we independently verify the validity of tuples for S and T .
I The postcondition for S must match the precondition for T .
If not, we can use weakening and strengthening rules.
35 / 60
Sequential Assignments
Let’s examine a verification for
fx = 5g x := x + 1; x := x + 1 fx > 6g
36 / 60
Sequential Assignments
Let’s examine a verification for
fx = 5g x := x + 1; x := x + 1 fx > 6g
36 / 60
Sequential Assignments
Let’s examine a verification for
fx = 5g x := x + 1; x := x + 1 fx > 6g
fP ^ B g S fQ g fP ^ :B g T fQ g
fP g if B then S else T end fQ g
Equivalently:
fP ^ B g S fQ g fP ^ :B g T fRg
fP g if B then S else T end fQ _ Rg
I Another instance of modular verification: we verify S and T
independently, assuming B and its negation :B in each case.
37 / 60
Taking Stock
fP g skip fP g
f[E x ]P g x := E fP g
=
P ) P 0 fP 0 g S fQ g fP g S fQ 0g Q 0 ) Q
fP g S fQ g fP g S fQ g
fP g S fQ g fQ g T fRg
fP g S ; T fRg
fP ^ B g S fQ g fP ^ :B g T fQ g
fP g if B then S else T end fQ g
I Given a precondition P and a precondition Q, our goal will be to
mechanically derive a command S such that fP g S fQ g.
I We examine further examples before giving the rule for while .
38 / 60
Outline
Mathematical Background
Hoare Logic
Triples
Assignments
Weakening and Strengthening
Sequential Composition and Conditionals
Examples of Annotations
Assignments
Conditionals
Exercise 5.6
Summary of Background
39 / 60
A First Annotation
We consider the following specification:
fP : x = X g
S
fQ : x = 3 X + 1g
What is S ? Based on Q, it is reasonable to implement S with an
assignment x := E , and to use the axiom f[E =x ]P g x := E fP g.
40 / 60
A First Annotation
We consider the following specification:
fP : x = X g
S
fQ : x = 3 X + 1g
What is S ? Based on Q, it is reasonable to implement S with an
assignment x := E , and to use the axiom f[E =x ]P g x := E fP g.
fP : x = X g
(* calculus *)
f3 x + 1 = 3 X + 1g
40 / 60
A First Annotation
We consider the following specification:
fP : x = X g
S
fQ : x = 3 X + 1g
What is S ? Based on Q, it is reasonable to implement S with an
assignment x := E , and to use the axiom f[E =x ]P g x := E fP g.
fP : x = X g
(* calculus *)
f3 x + 1 = 3 X + 1g
x := 3 x + 1
fQ : x = 3 X + 1g
Notice how we relate the program variable x and the specification
(logical) variable X . This is the style we shall adopt in the following.
40 / 60
Reversing the Assignment
fP : x = 3 X + 1g
S
fQ : x = X g
fP : x = 3 X + 1g
(* calculus *)
f(x 1) div 3 = X g
x := (x 1) div 3
fQ : x = X g
41 / 60
A More Interesting Annotation
fP : x = y 2 + X ^ y + 1 = Y g
S
fQ : x = y 2 + X ^ y = Y g
Based on Q, we start with the assignment y := y + 1.
We need to prepare it.
fP : x = y 2 + X ^ y + 1 = Y g
42 / 60
A More Interesting Annotation
fP : x = y 2 + X ^ y + 1 = Y g
S
fQ : x = y 2 + X ^ y = Y g
Based on Q, we start with the assignment y := y + 1.
We need to prepare it.
fP : x = y 2 + X ^ y + 1 = Y g
(* calculus: prepare y := y + 1 *)
42 / 60
A More Interesting Annotation
fP : x = y 2 + X ^ y + 1 = Y g
S
fQ : x = y 2 + X ^ y = Y g
Based on Q, we start with the assignment y := y + 1.
We need to prepare it.
fP : x = y 2 + X ^ y + 1 = Y g
(* calculus: prepare y := y + 1 *)
fx = (y + 1 1)2 + X ^ y + 1 = Y g
42 / 60
A More Interesting Annotation
fP : x = y 2 + X ^ y + 1 = Y g
S
fQ : x = y 2 + X ^ y = Y g
Based on Q, we start with the assignment y := y + 1.
We need to prepare it.
fP : x = y 2 + X ^ y + 1 = Y g
(* calculus: prepare y := y + 1 *)
fx = (y + 1 1)2 + X ^ y + 1 = Y g
y := y + 1;
fx = (y 1)2 + X ^ y = Y g
42 / 60
A More Interesting Annotation
fP : x = y 2 + X ^ y + 1 = Y g
S
fQ : x = y 2 + X ^ y = Y g
Based on Q, we start with the assignment y := y + 1.
We need to prepare it.
fP : x = y 2 + X ^ y + 1 = Y g
(* calculus: prepare y := y + 1 *)
fx = (y + 1 1)2 + X ^ y + 1 = Y g
y := y + 1;
fx = (y 1)2 + X ^ y = Y g
(* calculus *)
fx = y 2 2 y + 1 + X ^ y = Y g
42 / 60
A More Interesting Annotation
fP : x = y 2 + X ^ y + 1 = Y g
S
fQ : x = y 2 + X ^ y = Y g
Based on Q, we start with the assignment y := y + 1.
We need to prepare it.
fP : x = y 2 + X ^ y + 1 = Y g
(* calculus: prepare y := y + 1 *)
fx = (y + 1 1)2 + X ^ y + 1 = Y g
y := y + 1;
fx = (y 1)2 + X ^ y = Y g
(* calculus *)
fx = y 2 2 y + 1 + X ^ y = Y g
(* calculus *)
fx + 2 y 1 = y 2 + X ^ y = Y g
42 / 60
A More Interesting Annotation
fP : x = y 2 + X ^ y + 1 = Y g
S
fQ : x = y 2 + X ^ y = Y g
Based on Q, we start with the assignment y := y + 1.
We need to prepare it.
fP : x = y 2 + X ^ y + 1 = Y g
(* calculus: prepare y := y + 1 *)
fx = (y + 1 1)2 + X ^ y + 1 = Y g
y := y + 1;
fx = (y 1)2 + X ^ y = Y g
(* calculus *)
fx = y 2 2 y + 1 + X ^ y = Y g
(* calculus *)
fx + 2 y 1 = y 2 + X ^ y = Y g
x := x + 2 y 1
fQ : x = y 2 + X ^ y = Y g 42 / 60
A Conditional Command
fP : x max y = X ^ x min y = Y g
S
fQ : x = X ^ y = Y g
Note: We need not do anything if x y.
43 / 60
Conditional commands
fP : x max y = X ^ x min y = Y g
< y then
if x
fP ^ (x < y )g
fQ : x = X ^ y = Y g
else
fP ^ :(x < y )g
fQ : x = X ^y = Yg
end
fQ : x = X ^y = Yg
44 / 60
Conditional commands
fP : x max y = X ^ x min y = Y g
< y then
if x
fP ^ (x < y )g
(* P and calculus *)
fy = X ^ x = Y g
fQ : x = X ^ y = Y g
else
fP ^ :(x < y )g
fQ : x = X ^y = Yg
end
fQ : x = X ^y = Yg
44 / 60
Conditional commands
fP : x max y = X ^ x min y = Y g
< y then
if x
fP ^ (x < y )g
(* P and calculus *)
fy = X ^ x = Y g
z := x;
fy = X ^ z = Y g
fQ : x = X ^ y = Y g
else
fP ^ :(x < y )g
fQ : x = X ^y = Yg
end
fQ : x = X ^y = Yg
44 / 60
Conditional commands
fP : x max y = X ^ x min y = Y g
< y then
if x
fP ^ (x < y )g
(* P and calculus *)
fy = X ^ x = Y g
z := x;
fy = X ^ z = Y g
x := y;
fx = X ^ z = Y g
fQ : x = X ^ y = Y g
else
fP ^ :(x < y )g
fQ : x = X ^y = Yg
end
fQ : x = X ^y = Yg
44 / 60
Conditional commands
fP : x max y = X ^ x min y = Y g
< y then
if x
fP ^ (x < y )g
(* P and calculus *)
fy = X ^ x = Y g
z := x;
fy = X ^ z = Y g
x := y;
fx = X ^ z = Y g
y := z
fQ : x = X ^ y = Y g
else
fP ^ :(x < y )g
fQ : x = X ^y = Yg
end
fQ : x = X ^y = Yg
44 / 60
Conditional commands
fP : x max y = X ^ x min y = Y g
< y then
if x
fP ^ (x < y )g
(* P and calculus *)
fy = X ^ x = Y g
z := x;
fy = X ^ z = Y g
x := y;
fx = X ^ z = Y g
y := z
fQ : x = X ^ y = Y g
else
fP ^ :(x < y )g
(* :(x < y ) y x ; use P and calculus *)
fQ : x = X ^ y = Y g
fQ : x = X ^y = Yg
end
fQ : x = X ^y = Yg
44 / 60
Conditional commands
fP : x max y = X ^ x min y = Y g
< y then
if x
fP ^ (x < y )g
(* P and calculus *)
fy = X ^ x = Y g
z := x;
fy = X ^ z = Y g
x := y;
fx = X ^ z = Y g
y := z
fQ : x = X ^ y = Y g
else
fP ^ :(x < y )g
(* :(x < y ) y x ; use P and calculus *)
fQ : x = X ^ y = Y g
skip
fQ : x = X ^ y = Y g
end (* collect branches *)
fQ : x = X ^ y = Y g
44 / 60
Exercise 5.6(a)
fx = 3 X 2Y + 1 ^ y = Xg
S
fx = X ^ y = Y g
Implement S using an auxiliary variable h:
fx = 3 X 2Y + 1 ^ y = Xg
fx = X ^ y = Y g
45 / 60
Exercise 5.6(a)
fx = 3 X 2Y + 1 ^ y = Xg
S
fx = X ^ y = Y g
Implement S using an auxiliary variable h:
fx = 3 X 2Y + 1 ^ y = Xg
h := x ;
fh = 3 X 2Y + 1 ^ y = Xg
fx = X ^ y = Y g
45 / 60
Exercise 5.6(a)
fx = 3 X 2Y + 1 ^ y = Xg
S
fx = X ^ y = Y g
Implement S using an auxiliary variable h:
fx = 3 X 2Y + 1 ^ y = Xg
h := x ;
fh = 3 X 2Y + 1 ^ y = Xg
x := y ;
fh = 3 X 2Y + 1 ^ x = Xg
fx = X ^ y = Y g
45 / 60
Exercise 5.6(a)
fx = 3 X 2Y + 1 ^ y = Xg
S
fx = X ^ y = Y g
Implement S using an auxiliary variable h:
fx = 3 X 2Y + 1 ^ y = Xg
h := x ;
fh = 3 X 2Y + 1 ^ y = Xg
x := y ;
fh = 3 X 2 Y + 1 ^ x = Xg
(* calculus; substitute x = X *)
f2 Y = 3 x h + 1 ^ x = X g
fx = X ^ y = Y g
45 / 60
Exercise 5.6(a)
fx = 3 X 2Y + 1 ^ y = Xg
S
fx = X ^ y = Y g
Implement S using an auxiliary variable h:
fx = 3 X 2Y + 1 ^ y = Xg
h := x ;
fh = 3 X 2Y + 1 ^ y = Xg
x := y ;
fh = 3 X 2 Y + 1 ^ x = Xg
(* calculus; substitute x = X *)
f2 Y = 3 x h + 1 ^ x = X g
(* calculus; (2 Y ) div 2 = Y *)
fY = (3 x h + 1) div 2 ^ x = X g
fx = X ^ y = Y g
45 / 60
Exercise 5.6(a)
fx = 3 X 2Y + 1 ^ y = Xg
S
fx = X ^ y = Y g
Implement S using an auxiliary variable h:
fx = 3 X 2Y + 1 ^ y = Xg
h := x ;
fh = 3 X 2Y + 1 ^ y = Xg
x := y ;
fh = 3 X 2 Y + 1 ^ x = Xg
(* calculus; substitute x = X *)
f2 Y = 3 x h + 1 ^ x = X g
(* calculus; (2 Y ) div 2 = Y *)
fY = (3 x h + 1) div 2 ^ x = X g
y := (3 x h + 1) div 2
fx = X ^ y = Y g
45 / 60
Exercise 5.6(a): Variation
fx = 3 X 2Y + 1 ^ y = X g S fx = X ^ y = Y g
An alternative solution would use h differently:
fx = 3 X 2Y + 1 ^ y = Xg
fx = X ^ y = Y g
46 / 60
Exercise 5.6(a): Variation
fx = 3 X 2Y + 1 ^ y = X g S fx = X ^ y = Y g
An alternative solution would use h differently:
fx = 3 X 2 Y + 1 ^ y = Xg
(* substitute y = X *)
fx = 3 y 2 Y + 1 ^ y = X g
fx = X ^ y = Y g
46 / 60
Exercise 5.6(a): Variation
fx = 3 X 2Y + 1 ^ y = X g S fx = X ^ y = Y g
An alternative solution would use h differently:
fx = 3 X 2 Y + 1 ^ y = Xg
(* substitute y = X *)
fx = 3 y 2 Y + 1 ^ y = X g
(* calculus; (2 Y ) div 2 = Y *)
f(3 y x + 1) div 2 = Y ^ y = X g
fx = X ^ y = Y g
46 / 60
Exercise 5.6(a): Variation
fx = 3 X 2Y + 1 ^ y = X g S fx = X ^ y = Y g
An alternative solution would use h differently:
fx = 3 X 2 Y + 1 ^ y = Xg
(* substitute y = X *)
fx = 3 y 2 Y + 1 ^ y = X g
(* calculus; (2 Y ) div 2 = Y *)
f(3 y x + 1) div 2 = Y ^ y = X g
h := (3 y x + 1) div 2;
fh = Y ^ y = X g
fx = X ^ y = Y g
46 / 60
Exercise 5.6(a): Variation
fx = 3 X 2Y + 1 ^ y = X g S fx = X ^ y = Y g
An alternative solution would use h differently:
fx = 3 X 2 Y + 1 ^ y = Xg
(* substitute y = X *)
fx = 3 y 2 Y + 1 ^ y = X g
(* calculus; (2 Y ) div 2 = Y *)
f(3 y x + 1) div 2 = Y ^ y = X g
h := (3 y x + 1) div 2;
fh = Y ^ y = X g
x := y ;
fh = Y ^ x = X g
fx = X ^ y = Y g
46 / 60
Exercise 5.6(a): Variation
fx = 3 X 2Y + 1 ^ y = X g S fx = X ^ y = Y g
An alternative solution would use h differently:
fx = 3 X 2 Y + 1 ^ y = Xg
(* substitute y = X *)
fx = 3 y 2 Y + 1 ^ y = X g
(* calculus; (2 Y ) div 2 = Y *)
f(3 y x + 1) div 2 = Y ^ y = X g
h := (3 y x + 1) div 2;
fh = Y ^ y = X g
x := y ;
fh = Y ^ x = X g
y := h
fx = X ^ y = Y g
46 / 60
Exercise 5.6(b)
fx = 3 X 2Y + 1 ^ y = X g S fx = X ^ y = Y g
Implement S using only two assignments:
fx = 3 X 2Y + 1 ^ y = Xg
fx = X ^ y = Y g
47 / 60
Exercise 5.6(b)
fx = 3 X 2Y + 1 ^ y = X g S fx = X ^ y = Y g
Implement S using only two assignments:
fx = 3 X 2 Y + 1 ^ y = Xg
(* calculus; substitute y = X *)
fx = 3 X 2 Y + 1 ^ 3 y x +1 = 2Yg
fx = X ^ y = Y g
47 / 60
Exercise 5.6(b)
fx = 3 X 2Y + 1 ^ y = X g S fx = X ^ y = Y g
Implement S using only two assignments:
fx = 3 X 2 Y + 1 ^ y = Xg
(* calculus; substitute y = X *)
fx = 3 X 2 Y + 1 ^ 3 y x + 1 = 2 Y g
(* calculus; (2 Y ) div 2 = Y *)
fx = 3 X 2 Y + 1 ^ (3 y x + 1) div 2 = Y g
fx = X ^ y = Y g
47 / 60
Exercise 5.6(b)
fx = 3 X 2Y + 1 ^ y = X g S fx = X ^ y = Y g
Implement S using only two assignments:
fx = 3 X 2 Y + 1 ^ y = Xg
(* calculus; substitute y = X *)
fx = 3 X 2 Y + 1 ^ 3 y x + 1 = 2 Y g
(* calculus; (2 Y ) div 2 = Y *)
fx = 3 X 2 Y + 1 ^ (3 y x + 1) div 2 = Y g
y := (3 y x + 1) div 2;
fx = 3 X 2 Y + 1 ^ y = Y g
fx = X ^ y = Y g
47 / 60
Exercise 5.6(b)
fx = 3 X 2Y + 1 ^ y = X g S fx = X ^ y = Y g
Implement S using only two assignments:
fx = 3 X 2 Y + 1 ^ y = Xg
(* calculus; substitute y = X *)
fx = 3 X 2 Y + 1 ^ 3 y x + 1 = 2 Y g
(* calculus; (2 Y ) div 2 = Y *)
fx = 3 X 2 Y + 1 ^ (3 y x + 1) div 2 = Y g
y := (3 y x + 1) div 2;
fx = 3 X 2 Y + 1 ^ y = Y g
(* calculus; substitute y = Y *)
fx + 2 y 1 = 3 X ^ y = Y g
fx = X ^ y = Y g
47 / 60
Exercise 5.6(b)
fx = 3 X 2Y + 1 ^ y = X g S fx = X ^ y = Y g
Implement S using only two assignments:
fx = 3 X 2 Y + 1 ^ y = Xg
(* calculus; substitute y = X *)
fx = 3 X 2 Y + 1 ^ 3 y x + 1 = 2 Y g
(* calculus; (2 Y ) div 2 = Y *)
fx = 3 X 2 Y + 1 ^ (3 y x + 1) div 2 = Y g
y := (3 y x + 1) div 2;
fx = 3 X 2 Y + 1 ^ y = Y g
(* calculus; substitute y = Y *)
fx + 2 y 1 = 3 X ^ y = Y g
(* calculus; (3 X ) div 3 = X *)
f(x + 2 y 1) div 3 = X ^ y = Y g
fx = X ^ y = Y g
47 / 60
Exercise 5.6(b)
fx = 3 X 2Y + 1 ^ y = X g S fx = X ^ y = Y g
Implement S using only two assignments:
fx = 3 X 2 Y + 1 ^ y = Xg
(* calculus; substitute y = X *)
fx = 3 X 2 Y + 1 ^ 3 y x + 1 = 2 Y g
(* calculus; (2 Y ) div 2 = Y *)
fx = 3 X 2 Y + 1 ^ (3 y x + 1) div 2 = Y g
y := (3 y x + 1) div 2;
fx = 3 X 2 Y + 1 ^ y = Y g
(* calculus; substitute y = Y *)
fx + 2 y 1 = 3 X ^ y = Y g
(* calculus; (3 X ) div 3 = X *)
f(x + 2 y 1) div 3 = X ^ y = Y g
x := (x + 2 y 1) div 3
fx = X ^ y = Y g
47 / 60
The End
48 / 60
Outline
Mathematical Background
Hoare Logic
Triples
Assignments
Weakening and Strengthening
Sequential Composition and Conditionals
Examples of Annotations
Assignments
Conditionals
Exercise 5.6
Summary of Background
49 / 60
Notational matters
8x 2 V : P (x ) 8x (x 2 V ) P (x ))
9x 2 V : P (x ) 9x (x 2 V ^ P (x ))
50 / 60
Sets
I Empty set: ;
I Element: w 2 V means “w is member of the set V ”
I Standard notation: fx j P (x )g. Example:
fx j 0 x 3 100g = f0 1 2 3 4g
; ; ; ;
f2 x j x : 0 x 5g = f0 2 4 6 8 10g
; ; ; ; ;
fE (x ) j x : P (x )g = fy j 9x (y = E (x ) ^ P (x ))g
51 / 60
Integer division
10 div 3 = 3 ^ 10 mod 3 = 1
( 10) div 3 = 4 ^ ( 10) mod 3 = 2
I Identities:
z x div y z y x
x div y z x z y
< <
52 / 60
Conditional Expressions
I Conditional expression:
ord(b ) = (b ? 1 : 0)
53 / 60
Counting operator
54 / 60
Intervals
[m n ) = fk j m k n g
:: <
(m n ] = fk j m k n g
:: <
#[m n ) = #(m n ] = n
:: :: m
55 / 60
Maxima/Minima operators
The general case - Given a non-empty V :
a = Max V a 2 V ^ 8x (x 2 V ) x a )
a = Min V a 2 V ^ 8x (x 2 V ) a x )
Specific cases:
I empty set: Max ; = 1 and Min ; = 1
I singleton: Max fa g = Min fa g = a
I the binary operators max and min:
x max y = Max fx y g
; x min y = Min fx y g
;
I split rules:
(f (i ) j i 2 V )
to denote the family that consists of the values f (i ) for all i 2 V.
I Alternative notation: (f (i ) j i 2 V : P (i ))
I The family (f (i ) j i 2 V ) differs from the set ff (i ) j i 2 V g.
Example:
fi div 2 j i 2 [0 5)g = f0 1 2g
:: ; ;
(i div 2 j i 2 [0 5)) = (0 0 1 1 2)
:: ; ; ; ;
58 / 60
Operators on families
58 / 60
Distribution
I Multiplication over addition:
(x f (i ) j i 2 V ) = x (f (i ) j i 2 V )
I Addition over Max :
Max (x + f (i ) j i 2 V ) = x + Max (f (i ) j i 2 V )
I Addition over Min :
Min (x + f (i ) j i 2 V ) = x + Min (f (i ) j i 2 V )
I Multiplication over Max :
x 0 ^ V 6= ; ) Max (x f (i ) j i 2 V ) = x Max (f (i ) j i 2 V )
I Multiplication over Min :
x 0 ^ V 6= ; ) Min (x f (i ) j i 2 V ) = x Min (f (i ) j i 2 V )
59 / 60
Distribution
I Multiplication over addition:
(x f (i ) j i 2 V ) = x (f (i ) j i 2 V )
I Addition over Max :
Max (x + f (i ) j i 2 V ) = x + Max (f (i ) j i 2 V )
I Addition over Min :
Min (x + f (i ) j i 2 V ) = x + Min (f (i ) j i 2 V )
I Multiplication over Max :
x 0 ^ V 6= ; ) Max (x f (i ) j i 2 V ) = x Max (f (i ) j i 2 V )
I Multiplication over Min :
x 0 ^ V 6= ; ) Min (x f (i ) j i 2 V ) = x Min (f (i ) j i 2 V )
Notice:
I x <0^V 6= ; ) Max (x f (i ) j i 2 V ) = x Min (f (i ) j i 2 V )
I x < 0^V =6 ; ) Min (x f (i ) j i 2 V ) = x Max (f (i ) j i 2 V )
59 / 60
Quantifiers and Predicates
(8x 2 V : Q _ P (x )) Q _ (8x 2 V : P (x ))
(9x 2 V : Q ^ P (x )) Q ^ (9x 2 V : P (x ))
60 / 60