worksheet_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 represented as “:=”,
as in “X := X+1”) is NOT the same as the concept of mathematical equality
(usually represented as “=”, as 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? Circle either “would” or “would not” as
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, z≤-5)  (y=z+1) would would not



2. (6 pts.) Circle either “valid” or “invalid” for 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:33:35 GMT -05:00


https://www.coursehero.com/file/131962273/worksheet-8pdf/

, 2
3. (8 pts.) Circle either “true” or “false” for 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} S {Q}
b. (3 pts.) Give the “preservation” antecedent of the repeat_until statement ROI with
consequent {P} repeat s until b {Q} that you were asked to prove in problem 4 of the
Assignment 7 Worksheet:

“preservation” antecedent: ________________________

c. (8 pts.) Use the ROI from part (a) to prove the “preservation” antecedent of part (b) using
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 your proof on the next page…

(cont’d)

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


https://www.coursehero.com/file/131962273/worksheet-8pdf/