1

Lectures 20 and 21

Weakest Pre-Condition for While Statement and Intro to Functional Verification

This week we look at the problem of deriving weakest (liberal) pre-conditions and strongest post-conditions for while statements. We also discover an interesting connection between w(l)p’s and loop invariants (“Predicate Transforms II”). Following this, we shift our attention to functional verification, beginning with the notion of complete vs. sufficient program correctness (“Functional Verification I”).

Predicate Transforms II

Context:

Although the transform rules for while statement are reasonably straightforward, finding a regularity in the terms that yields a closed-form expression (i.e., one comprised of a finite number of terms) is comparable to identifying a loop invariant. In fact, for wp’s, the result turns out to be the weakest invariant which guarantees program termination in state Q!

Purpose:

To extend the transform rules presented in theprevious lecture to while statements, and to illustrate the connection between weakest (liberal) pre-conditions and loop invariants.

Competency Objectives:

At the end of this lesson, you will be able to:

  1. Derive an expression for the weakest (liberal) pre-condition and strongest post-condition of a while_do statement.
  2. Find obvious regularities in the terms of open-form transform expressions that allow a closed-form (finite) expression.

Key Points:

  1. wp(while b do S, Q) H0V H1 V H2 V… where:

H0 ¬b Л Q

H1 b Л wp(S, H0)

H2 b Л wp(S, H1)

:

Hi b Л wp(S, Hi-1)

:

  1. wlp(while b do S, Q)  wp(while b do S, Q) V ¬wp(while b do S, true)
  2. sp(while b do S, P)  ¬b Л (K0 V K1 V K2 V ...)where

K0 P

K1 sp(S, b Л K0)

K2 sp(S, b Л K1)

:

KN  sp(S, b Л KN-1)

:

  1. wp(while b do S, Q) is the weakest loop invariant which guarantees termination of S.
  2. wlp(while b do S, Q) is the weakest loop invariant which does NOT guarantees termination of S.

Functional Verification I

Context:

Next, we consider afunction-theoretic based approach for determining the correctness of structured, sequential program. Correctness is defined as a correspondence between a program and its intended function.

Purpose:

The purpose of this first of four lectures on functional verification is to (1) illustrate the equivalence of tasks associated with reading (i.e., attempting to understand), writing, and verifying programs in the context of function-theoretic verification; (2) explain the distinction between complete and sufficientprogramcorrectness, and (3) introduce the Axiom of Replacement which allows proving the correctness of a compound program in a stepwise fashion.

Competency Objectives:

At the end of this lesson, you will be able to:

  1. Explain why the tasks encountered in reading, writing, and verifying programs are identical.
  2. Determine the correctness relations (complete/sufficient, sufficient only, or neither) between simple programs and given functions.
  3. Explain how the Axiom of Replacement allows the stepwise verification of compound programs.

Key Points:

  1. The tasks in program reading, writing, and verification are identical. In all three cases, we seek to confirm the equivalence (or subset relationship) of two expressions, each representing the function of a program.
  2. In the case of complete correctness of program P with respect to function f, P computes values for arguments in D(f) only;P is undefined for arguments outside D(f);in the case ofsufficient correctness, P may compute values from arguments not in D(f).
  3. Henceforth, we will follow the lead of Dunlop and Basili (“A Comparative Analysis of Functional Correctness”) and adopt the convention of asserting “P computes f” if and only if f is a subset of [P], i.e., an assertion of sufficient correctness.Thus, for “P to compute f”(which we will now write informally as “f=[P]”), no explicit requirement is made concerning the behavior of P on inputs outside the domain of f.
  4. To show that compound program F implements function f, where F incorporates (sub-)programs G and H: hypothesize functions g, h and attempt to prove g = [G] and h = [H]. If successful, use the Axiom of Replacement to reduce the problem to proving F,with functions g and h replacing (sub-)programs G and H, implements function f.

Self-Check Quiz Questions

  1. (6 pts.) Determine the weakest pre-condition of:

while x>0 do

y := y+1

x := x−1

end_while

with respect to the post-condition: x=0 Л y=y0+x0. Show the values of H0, H1, H2, and Hk, and then express the result in closed form (without reference to "k").

2. (10 pts.) Use the strongest post-condition ROI to prove:

{i=1 Л t=1 Л x=1}

while i>3 do

t := t*x

i := i+1

end_while

{t=x5}

3. (4 pts.) Determine the correctness relationships betweenprogram P and each of

the functions below. Indicate "C" forComplete (and Sufficient), "S" for Sufficient

only, or "N" for Neither. (Note that"I" is the "Identify" function. E.g., x,y,z :=

x,y,z)

P = while x>0 do

x := x-1

y := y+2

end_while

a. f1 = (x>0 -> x,y := 0,y+2x | true -> I)

b. f2 = (x>0 -> x,y := 0,y+2x)

c. f3 = (x>=0 -> x,y := 0,y+2x)

d. f4 = (x>0 -> x,y := 0,y+2x | x=0 -> I)