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