SOFTWARE VERIFICATION

Goal: Ensure that Software Meets its Specifications

How: Analysis, Program Proving, Testing, Measurements, . . .

 

PROGRAM PROVING WITH HOARE LOGIC

Basis: Prove that

If assertion P is true before executing program or statement

S, and S halts, then assertion Q is true after executing S.

P is a precondition, Q a postcondition.

Notation: {P} S {Q}

Use Axioms and Proof Rules.

(Separately, prove that S halts.)

 

• Axiom of Assignment: { Px ¨ expr } x := expr { P }

 

• Rules of Consequence:

If {P} S {Q} and QfiR, then {P} S {R}.

If {P} S {Q} and RfiP, then {R} S {Q}.

 

• Rule of Composition (Compound Statements)

If {P} S1 {Q} and {Q} S2 {R}, then {P} S1; S2 {R}.

 

 

 

• Rule for Conditionals: if/then/else

If {P Ÿ B} S1 {Q} and {P Ÿ ÿB} S2 {Q}, then

{P} if B then S1 else S2 {Q}

 

• Rule for Iteration : while Statement

If { P Ÿ B} S {P}, then {P} while B do S {P Ÿ ÿB}

P is the loop invariant.

 

• EXAMPLE

Program to find an integer approximation to sqrt(N)

where N is a positive integer.

P: {N ≥ 0, N an integer}

a := 0 ; while (a+1)≠2 £ N do a := a + 1;

Q: { a≠2 £ N Ÿ (a+1)≠2 > N}

Program Specification given by P and Q.

The loop invariant: { a≠2 £ N }

 

• Practical Use of Program Proving Techniques