Software Testing & Verification Assignment 4 Group Activity Worksheet KEY

Document Content and Description Below

Software Testing & Verification Assignment 4 Group Activity Worksheet KEY 1. (6 pts.) Which one of the following is the most appropriate interface specification based on pre- and post-conditions fo ... r a program that sets variable ILIK to the Index of the Last Instance of K in the non-empty, unsorted array A[1:N] (where N is an integer constant), or to -1 if K is not an instance of A. a. pre-condition: {N≥1 Λ for every 1≤j<N, ¬(A[j]<A[j+1] V A[j]>A[j+1])} post-condition: {[(1≤ILIK≤N Λ A[ILIK]=K Λ for every ILIK<j≤N, A[j]≠K) V (for every 1≤j≤N, ILIK=-1)] Λ UNCH(A,K)} b. pre-condition: {N≥1} post-condition: {[(1≤ILIK≤N Λ A[ILIK]=K Λ for every ILIK<j≤N, A[j]≠K) V ILIK=-1] Λ UNCH(A,K)} c. pre-condition: {N≥1} post-condition: {[(for every 1≤j≤N, A[j]=K Λ ILIK=N) V (for every 1≤j≤N, A[j]≠K) Λ ILIK=-1] Λ UNCH(A,K)} d. pre-condition: {N≥1} post-condition: {[(ILIK=N Λ A[N]=K) V ILIK=-1] Λ UNCH(A,K)} e. pre-condition: {N≥1} post-condition: {[(1≤ILIK≤N Λ A[ILIK]=K Λ for every 1≤j<ILIK, A[j]≠K) V (for every 1≤j≤N, A[K]≠-1) Λ ILIK=-1] Λ UNCH(A,K)} f. pre-condition: {N≥1} post-condition: {[(1≤ILIK≤N Λ A[ILIK]=K Λ for every ILIK<j≤N, A[j]≠K) V (for every 1≤j≤N, A[j]≠K Λ ILIK=-1)] Λ UNCH(A,K)} g. pre-condition: {N≥1} post-condition: {[(1≤ILIK≤N Λ A[ILIK]=K Λ for every 1≤j<ILIK, A[j]≠K) V (for every 1≤j≤N, A[j]≠K) Λ ILIK=-1] Λ UNCH(A,K)} 2. (4 pts.) Which one of the following most accurately reflects the meaning of the weak correctness predicate, "{P} S {Q}"? (Circle ONE only.) a. ( {P} S {Q} ) ≡ “P must hold before S executes and Q must hold when S terminates” b. “Q could be false when S terminates” ≡ ¬( {P} S {Q} ) c. If P holds before executing S, S must terminate in state Q. d. {P} S {Q} ≡ [(“P is false before S executes”) V (“S does not terminate”) V “Q must be true when S terminates given that P is true before S executes”) e. {P} S {Q} is true unless Q is always false when S terminates, given that P is true before S executes. f. (none of the above) 2 3. (10 pts.) Consider the assertion of weak correctness: {x>0} S {y=z+x}. Which of the following facts would logically imply that this assertion is FALSE and which would not? Circle either “would” or “would not” as appropriate. Consider each fact given independently. To compensate for random guessing, you will receive +2 pts. for each correct answer and -2 pts. for each incorrect answer. a. When the initial value of x is -5, S terminates with y=z+x. would would not b. When the initial value of x is 5, S terminates with y=z. would would not c. For all initial values of x<10, S terminates with the final would would not value of y being less than z+x. d. For at least one initial value of x satisfying the given would would not pre-condition, S terminates with y=z-x. e. Whenever the initial value of x is greater than -5, S does would would not not terminate. 4. (20 pts.) Circle either “true” or “false” for each of the following assertions. Note that to compensate for random guessing, you will receive +2 pts. for each correct answer and -2 pts. for each incorrect answer. a. [{x=17} S {x=17}]  [{x>0} S {x>0}] true false b. [{x>0} S {x=17}]  [{x=17} S {x>0}] true false c. {z=x(y-n)} y := y+1 {z-x=x(y-n)} true false [Show More]

Last updated: 2 years ago

Preview 1 out of 4 pages