CEN 6070 Software Test Verifi - University of Florida - CEN 6070 Software Testing & Verification

Document Content and Description Below

CEN 6070 Software Testing & Verification Consider the assertion of weak correctness: {a=b V b>0} S {a+b=c Λ b<0}. Which of the following observations/facts would allow one to deduce that the assert... ion is false, and which would not? Circle either “would” or “would not” as appropriate, considering the observations individually. To compensate for random guessing, your score in points will be 2 times the number of [correct minus incorrect] answers, or 0 – whichever is greater. Therefore, if you are not more than 50% sure of your answer, consider skipping the problem. a. sp(S, b=5) = (a=c) would would not b. If a=-5 and b2=25 prior to the execution of S, then S would would not terminates with c=17. c. wlp(S, a>c) = (ab<0 Λ a>0) would would not d. wp(S, a<c) = (ab>0 Λ a>0) would would not e. When the initial value of b is 17, S does not terminate. would would not f. S sometimes terminates with b=17 when the initial value would would not of b is -17. g. S always terminates with b=17 when the initial value would would not of b is -17. h. wlp(S, a+b=c Λ b<0) ≠ (a=b V b>0) would would not 2 2. (18 pts.) Circle either “true” or “false” for each of the following assertions. To compensate for random guessing, your score in points will be 2 times the number of [correct minus incorrect] answers, or 0 – whichever is greater. Therefore, if you are not more than 50% sure of your answer, consider skipping the problem. a. If K = wp(S, Z), then sp(S,K) Z. true false b. If K wp(S, Z), then sp(S,K) = Z. true false c. Assuming S terminates whenever K holds true false initially, if sp(S,K) Z, then K = wp(S,Z). d. Assuming S terminates whenever K holds true false initially, if sp(S,K) = Z, then K wp(S,Z). e. Suppose K = wp(while b do S, Q). Then K is a Q- true false adequate loop invariant for {K} while b do S {Q}. f. {P} while b do S {Q} {P} true false if b then repeat S until NOT b end_if {Q} g. The Method of Well Founded Sets, as presented true false in class, cannot be used to prove that the program below will terminate for some initial values of x,y. while (y>0) do y := y+x if (x≥0) then x := x-1 end_if end_while h. Formally speaking, Z=XJ is a loop invariant true false for the assertion: {Z=0 Λ X=0} while J<Y do Z := Z+X; J := J+1 end_while {Z=XY} i. Z=XJ Λ J≤Y is a Q-adequate loop invariant true false for the assertion given in part (h) above. 3 3. a. (2 pts.) Complete the ROI for proving the weak correctness of program S with respect to pre-condition P and post-condition Q using the weakest liberal precondition (wlp) predicate transform: {P} S {Q} b. (4 pts.) Identify expressions for H1, H2, H3, and Hk such that wp(Repeat s Until c, Q) = H1 V H2 V H3 V...V Hk V... where Hi represents the necessary and sufficient condition that "Repeat s Until c" terminates in state Q after i executions of s. (Hint: for i>1, Hi should be expressed as a function of Hi-1.) : c. (15 pts.) Find the weakest liberal pre-condition (wlp) of the program: K: Repeat z := z+y; t := t-1 Until t=0 with respect to the post-condition {z=yx}. (Give the values of H1, H2, and Hk, where the wp(K, z=yx) is given by the infinite expression: H1 V H2 V ... V Hk V ... and then express the wlp(K, z=yx) in closed form.) ASSUME that wp(K, true) is t>0. Closed form expression of w 4 3. (cont’d) d. (6 pts.) Use the ROI from part (a) and the closed form expression of the wlp from part (c) to prove the assertion: {t=2 Λ x=6 Λ z=8 Λ y=2} Repeat z := z+y; t := t-1 Until t=0 {z=yx} Note that, by observation, the values of both x and y are invariant with respect to program K. [Show More]

Last updated: 1 year ago

Preview 1 out of 10 pages