Milind_Jayan_handout_8 University of Florida CEN 6070

Software Testing & Verification
Assignment 8 Worksheet

NOTE: ATTEMPT TO PROVIDE ANSWERS FOR ALL PROBLEMS. IF YOU DO NOT
UNDERSTAND A PROBLEM, REVIEW THE RELEVANT LECTURE NOTES AND/OR SEEK
HELP FROM OTHER SOFTWARE TESTING & VERIFICATION STUDENTS (VIA POSTS IN
THE ASSIGNMENT 8 DISCUSSION SPACE, FOR EXAMPLE).

Remember: an assignment operation in a program (often ep e en ed a := ,
as in X := X+1 ) is NOT the same as the concept of mathematical equality
( all ep e en ed a = , a in {2=X Л 5>Z ). DO NOT INTERCHANGE THESE
SYMBOLS!


1. (9 pts.) Consider the assertion of strong correctness: {z<0} S {y=z+1} strongly, where z
and y are integers. Which of the following observations/facts would allow one to deduce that
the assertion is false, and which would not? C c e e he d d a
appropriate, considering the observations individually. To compensate for random guessing,
you will receive +3 pts. for each correct answer and -3 pts. for each incorrect answer.

a. wp(S, y=z+1) = {z>-5} would would not


b. wp(S, y z) = {z>-5} would would not


c. sp(S, -5) (y=z+1) would would not



2. (6 .) C c e e he a d a d f each of the following hypothesized Rules of
Inference. To compensate for random guessing, you will receive +2 pts. for each correct
answer and -2 pts. for each incorrect answer.

sp(S, P) Q
a. ----------------------------------------------------------------------- ? valid invalid
{P} S {Q} strongly


Q sp(S, P)
b. ----------------------------------------------------------------------- ? valid invalid
{true} S {Q}


(wlp(S, Q) K) P
c. ----------------------------------------------------------------------- ? valid invalid
{P} S {Q}




This study source was downloaded by 100000850872992 from CourseHero.com on 04-08-2023 16:35:33 GMT -05:00


https://www.coursehero.com/file/70861455/Milind-Jayan-handout-8pdf/

, 2
3. (8 .) C c e e he e fa e f each of the following assertions. To compensate for
random guessing, you will receive +2 pts. for each correct answer and -2 pts. for each
incorrect answer.

a. If sp(S,P), when defined, is at least as strong as Q, then P holds true false
initially and Q holds if S terminates.


b. K=wp(S, true) S terminates if and only if K is true before S true false
executes


c. sp(temp := x; x := y; y := temp, true) true false
sp(y := y+x; x := y-x; y := y-x, true)


d. sp(x := x+1, x<n) = x<n+1 true false


4. a. (3 pts.) Complete the ROI below for proving {P} S {Q} using a weakest liberal pre-
condition (wlp) predicate transform:

ROI:
P wlp ( s ,


{P} S {Q}
b. (3 .) G e he e e a a ecede f he e ea _ a e e ROI h
consequent {P} repeat s until b {Q} that you were asked to prove in problem 8(b) of the
Assignment 7 Worksheet:

e e a a ecede In { b I }s{
: ________________________
-
}
c. (8 .) U e he ROI f a (a) e he e e a a ecede f a (b) g
the invariant I: y=t-x Л a=4 for the following assertion:

{x=t y=0}
repeat
y := y+1;
x := x-1;
a := 4
until x=0
{y=t a=4}

EXPLICITLY SHOW EACH INDIVIDUAL STEP OF YOUR PROOF AS ILLUSTRATED
IN THE LECTURE NOTES i.e., DO NOT SKIP OR COMBINE ANY STEPS. (IN PARTICULAR,
CONSIDER THE EFFECT OF EACH ASSIGNMENT STATEMENT IN THE LOOP BODY
INDIVIDUALLY.)

Provide f he e age

(c d)

This study source was downloaded by 100000850872992 from CourseHero.com on 04-08-2023 16:35:33 GMT -05:00


https://www.coursehero.com/file/70861455/Milind-Jayan-handout-8pdf/