CEN5035_Worksheet University of Florida CEN 5035

Software Testing & Verification
Assignment 9 Group Activity Worksheet -- Solutions

1. (10 pts.) Which of the following expressions are propositions and which are predicates? Circle
at most one answer for each part. (You will receive +2 pts. for each correct answer and -1
pt. for each incorrect answer.)
a. Object X is a duck proposition predicate cannot determine
b. Mickey Mouse is a duck proposition predicate cannot determine
c. At least one object X proposition predicate cannot determine
is a duck.
d. There is at least one duck proposition predicate cannot determine
that likes to eat Y.
e. There is at least one cow that proposition predicate cannot determine
actively promotes eating more
chicken.

2. (3 pts.) What is the difference, if any, between the following two logical expressions?
A, B, C
──────── (A Λ B Λ C)  D
D

Their logical interpretation is identical, but the “Rule of Inference” form on the left implies that
the writer believes the conditional statement to be True (i.e., valid).




3. (6 pts.) Give an appropriate pre- and post-condition for a program that sets variable I to the
index of the first instance of Y in the non-empty array A[1:N], or to -1 if Y is not an element
of array A[1:N].

pre-condition: {N≥1}

post-condition: {[(1≤I≤N AND A[I]=Y AND for every 1≤k<I, A[k]<>Y) OR
(for every 1≤k≤N, A[k]<>Y) AND I=-1] AND UNCH(A,Y)}




4. (6 pts.) Give a conditional function comprised of two (predicate -> rule) pairs using
concurrent assignment functions for the following program: if x>0 then x := x-3;
y := x+3 end_if

f = (x>0  x,y := x-3,x | x≤0  x,y := x,y)



This study source was downloaded by 100000850872992 from CourseHero.com on 04-09-2023 01:27:17 GMT -05:00


https://www.coursehero.com/file/50533280/Assignment-9-Worksheet-solpdf/