Software Testing & Verification Assignment 4 Group Activity Worksheet KEY University of Notre Dame MANAGEMENT ADBI4211

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 for 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)



This study source was downloaded by 100000850872992 from CourseHero.com on 04-02-2023 01:22:32 GMT -05:00


https://www.coursehero.com/file/145153079/sp22-Assignment-4-worksheet-key-5pdf/