Proofs of Correctness: Introduction
to Axiomatic Verification
Introduction
Weak correctness predicate
Assignment statements
Sequencing
Selection statements
Iteration
1
Introduction
What is Axiomatic Verification?
A formal method of reasoning about the
functional correctness of a structured,
sequential program by tracing its state
changes from an initial (i.e., pre-) condition
to a final (i.e., post-) condition according to
a set of self-evident rules (i.e., axioms).
What is its primary goal?
To provide a means for “proving” (or
“disproving”) the functional correctness of a
sequential program with respect to its
(formal) specification.
2
1
Introduction (cont.)
What are the benefits of studying
axiomatic verification?
Understanding its limitations.
Deeper insights into programming and
program structures.
Criteria for judging both programs and
programming languages.
The ability to formally verify small (or
parts of large) sequential programs.
Weak Correctness Predicate
To prove that program S is (weakly)
correct with respect to pre-condition P
and post-condition Q, it is sufficient to
show: {P} S {Q}.
Interpretation of {P} S {Q}: “if the
input (initial state) satisfies the pre-
condition P and (if) the program S
executes and terminates, then the
output (final state) will satisfy the
post-condition Q.”
2
Weak Correctness Predicate (cont.)
Thus, {P} S {Q} is true unless
Q could be false if S
terminates, given that P held
before S executes.
What are the truth values of
the following assertions?
(1) {x=1} y := x+1 {y>0}
(2) {x>0} x := x-1 {x>0}
5
Weak Correctness Predicate (cont.)
Thus, {P} S {Q} is true unless
Q could be false if S
terminates, given that P held
before S executes.
What are the truth values of
the following assertions?
(3) {1=2} k := 5 {k<0}
3
Weak Correctness Predicate (cont.)
Thus, {P} S {Q} is true unless Q
could be false if S terminates,
given that P held before S executes.
What are the truth values of the
following assertions?
(4) {true} while x <> 5 do x := x-1 {x=5}
(Hint: When will S terminate?)
Weak Correctness Predicate (cont.)
We now consider techniques for
proving that such assertions hold for
structured programs comprised of
assignment statements, if-then (-
else) statements, and while loops.
(Why these particular constructs?)
4
Reasoning about Assignment
Statements
For each of the following pre-
conditions, P, and assignment
statements, S, identify a “strong”
post-condition, Q, such that {P} S {Q}
would hold.
A “strong” post-condition captures all
after-execution state information of
interest.
We ignore propositions such as X=X’
(“the final value of X is the same as
the initial value of X”).
9
Reasoning about Assignment
Statements (cont.)
{P} S {Q}
{J=6} K := 3
{J=6} J := J+2
{A<B} Min := A
{X<0} Y := -X
10
5
Reasoning about Assignment
Statements (cont.)
For each of the following post-
conditions, Q, and assignment
statements, S, identify a “weak”
pre-condition, P, such that
{P} S {Q} would hold.
(A “weak” pre-condition reflects
only what needs to be true
before.)
11
Reasoning about Assignment
Statements (cont.)
{P} S {Q}
I := 4 {J=7 Λ I=4}
I := 4 {I=4}
I := 4 {I=17}
Y := X+3 {Y=10}
12
6
When does
({P} S {Q}) ⇒ ({K} S {W})?
We just determined that
{J=7} I := 4 {J=7 Λ I=4}
holds.
We can deduce from this that
{J=7} I := 4 {J=7}
also holds since {J=7 Λ I=4} is stronger
than {J=7}, because
{J=7 Λ I=4} ⇒ {J=7}.
13
When does
({P} S {Q}) ⇒ ({K} S {W})?
Similarly, if we know that
{J=7} I := 4 {J=7 Λ I=4}
holds, it follows that
{J=7 Λ K=17} I := 4 {J=7 Λ I=4}
also holds since {J=7} is weaker than
{J=7 Λ K=17}, because
{J=7 Λ K=17} ⇒ {J=7}.
14
7
When does
({P} S {Q}) ⇒ ({K} S {W})?
Thus, we can replace pre-
conditions with ones that are
stronger, and post-conditions
with ones that are weaker.
Note that if A ⇒ B, we say that A
is stronger than B, or
equivalently, that B is weaker
than A.
15
Reasoning about Sequencing
In general:
if you know {P} S1 {R} and
you know {R} S2 {Q}
then you know {P} S1; S2 {Q}.
(So, to prove {P} S1; S2 {Q}, find {R}.)
16
8
Example 1
Prove the assertion:
{A=5} B := A+2; C := B-A; D := A-C {A=5 Λ D=3}
17
Reasoning about If_then_else
Statements
Consider the assertion:
{P} if b then S1 else S2 {Q}
{P}
T F
b
S1 S2
{Q}
What are the necessary conditions for
this assertion to hold?
18
9
Reasoning about If_then
Statements
{P}
Consider the assertion:
T
{P} if b then S {Q} b
F
S
What are the necessary
conditions for this assertion to {Q}
hold?
19
Example 2
Prove the assertion:
{Z=B} if A>B then Z := A {Z=Max(A,B)}
20
10
Proof Rules
Before proceeding to while loops, let’s
capture our previous reasoning about
sequencing, selection statements, and
state condition replacement in
appropriate rules of inference.
Rule for Sequencing:
{P} S1 {R}, {R} S2 {Q}
{P} S1; S2 {Q}
21
Proof Rules (cont.)
Rule for if_then_else statement:
{P Λ b } S1 {Q}, {P Λ ¬b} S2 {Q}
{P} if b then S1 else S2 {Q}
Rule for if_then statement:
{P Λ b } S {Q}, (P Λ ¬b) ⇒ Q
{P} if b then S {Q}
22
11
Proof Rules (cont.)
Rule for State Condition Replacement:
K ⇒ P, {P} S {Q}, Q ⇒ W
{K} S {W}
23
Reasoning about Iteration
{P}
Consider the assertion:
{P} while b do S {Q}
F
b
T
S
What are the necessary
conditions for this
{Q}
assertion to hold?
24
12
Consider a Loop “Invariant” - I
{P} Suppose I holds initially…
I
F
b
IЛb T
I Л ¬b and implies Q
S when and if the
loop finally
is preserved by S… terminates…
I {Q}
then the assertion
would hold!
25
Sufficient Conditions: while_do
Thus, a Rule for the while_do statement
is:
P ⇒ I, {I Λ b} S {I}, (I Λ ¬b) ⇒ Q
{P} while b do S {Q}
where the three antecedents are
sometimes given the names
initialization, preservation, and
finalization, respectively.
26
13
Example 3
Use the invariant I: Z=XJ to prove:
{true} Initialization: P ⇒ I
Z := X Preservation: {I Λ b} S {I}
J := 1 Finalization: (I Λ ¬b) ⇒ Q
while J<>Y do
Z := Z+X
J := J+1
end_while
{Z=XY}
27
Example 3
Use the invariant I: Z=XJ to prove:
{true}
Initialization: P ⇒ I
Z := X
J := 1 What is “P” ?
P
while J<>Y do (Z=X Λ J=1)
Z := Z+X Does
J := J+1
end_while (Z=X Λ J=1) ⇒ Z=XJ ?
{Z=XY} Yes!
28
14
Example 3
Use the invariant I: Z=XJ to prove:
Initialization: P ⇒ I √
{true} Preservation: {I Λ b} S {I}
Z := X b {Z=XJ Λ J ≠Y}
J := 1 Z := Z+X
while J<>Y do {Z=X(J+1) Λ J ≠Y}
Z := Z+X J := J+1
J := J+1 S {Z=X((J-1)+1) Λ J-1≠Y}
end_while ⇒ Z=XJ
{Z=XY}
29
Example 3
Use the invariant I: Z=XJ to prove:
Initialization: P ⇒ I √
{true}
Preservation: {I Λ b} S {I} √
Z := X
J := 1 Finalization: (I Λ ¬b) ⇒ Q
while J<>Y do
Z := Z+X Does (Z=XJ Λ J=Y) ⇒ Z=XY?
J := J+1
end_while Yes!
{Z=XY}
30
15
Example 3
Use the invariant I: Z=XJ to prove:
{true} Initialization: P ⇒ I √
Z := X Preservation: {I Λ b} S {I} √
J := 1 Finalization: (I Λ ¬b) ⇒ Q √
while J<>Y do
Z := Z+X
J := J+1
end_while
{Z=XY}
31
Some Limitations of Formal
Verification
Difficulties can arise when dealing
with:
parameters
pointers
synthesis of invariants
decidability of verification conditions
concurrency
32
16
Some Limitations of Formal
Verification (cont.)
In addition, a formal specification:
may be expensive to produce
may be incorrect and/or incomplete
normally reflects functional
requirements only
Will the proof process be manual
or automatic? Who will prove the
proof?
33
17
