• University of Florida

• CEN 6070

 Software Testing & Verification

Assignment 16 Group Activity Worksheet

1. (5 pts.) Derive the weakest f-adequate loop invariant q(X)=( f(X)=f(X0) ) over D(f) for

programs of the form while p do g that compute f = (x≥0  x,y := 0,y+2x). Determine

q(X) by equating f(X) with f(X0) for variables x and y as shown in class. Your expression for

the invariant q should be in the form: y = (an expression of y0, x0, and x) Л x≥0 since f is

defined for x≥0 only.

y = y0 + 2(x0 – x) Л x≥0

2. Consider program K: while x<>0 do y := y+2; x := x-1 end_while

a. (14 pts.) Prove that K computes f (from problem 1) using the corollary of the Invariant

Status Theorem as captured in the following ROI:

term(f,K) Л q(X) is an f-adequate invariant of K

────────────────────────────────────

f = [K]

Since K obviously terminates when x≥0, you need NOT prove term(f,K). To show that q is

an f-adequate invariant of K, you must, however, show:

(1) ( q(X) Л p(X) )  qog(X), and (2) ( q(X) Л ¬p(X) )  ( X=f(X0) )

To show ( q(X) Л p(X) )  qog(X), follow these steps:

(i) AND your q from problem (1) WITH p (the predicate of K) to yield qΛp. Simplify by

combining x≥0 and p into a single term.

y=y0+2(x0–x) Л x>0

(ii) Compose your q from problem (1) with g (the body of K) to yield qog by replacing

each occurrence of x and y in q with the new values assigned to x and y by g.

Simplify.

y=y0+2(x0-x) Л x>0

(iii) Finally, argue that your qΛp from step i implies your qog from step ii.

Clearly, [q(X)Лp(X) = (y=y0+2(x0–x) Л x>0)]  [qog(X) = (y=y0+2(x0–x) Л x>0)]

To show ( q(X) Л ¬p(X) )  ( X=f(X0) ), follow these steps:

(iv) AND your q from problem (1) WITH ¬p (the negation of predicate of K) to yield

qΛ¬p. Simplify by combining x≥0 and ¬p into a single term.

(y=y0+2(x0–x) Л x=0)

(v) Argue that your qΛ¬p implies y=fy(x0, y0) Л x=fx(x0, y0) which is equivalent to X=f(X0)

qΛ¬p  (y=y0+2x0 Л x=0)  [y=fy(x0, y0) Л x=fx(x0, y0)] ≡ X=f(X0)

This study source was downloaded by 100000853497421 from CourseHero.com on 04-23-2023 01:44:26 GMT -05:00

https://www.coursehero.com/file/50534395/Assignment-16-Worksheet-solpdf/

2

3. a. (4 pts.) Give the sequence of states X0, X1, ..., Xn produced by each iteration of K (from

problem 2) given that the initial state, X0 = (x0,y0) = (3,3) and Xn is the final state.

X0 = (3,3), X1 = (2,5), X2 = (1,7), X3 = Xn = (0,9)