3
------CEN 4072/6070 Software Testing & Verification ------
Exam 2 – Spring 2010
Note: there are two versions of Exam 2. These solution notes correspond to the exam posted. Students will be provided with a copy of the correct solution notes for their exam when viewed.
1. false, false, true, true, false, true, true, false
2. true, true, true, false, false, false, true, false
3. nec. true, not nec. true, nec. true, not nec. true, nec. true
4. f. initialization and preservation only
5.
P1 / P2 / P3f1 / N / S / C
f2 / N / C / N
6. d. initialization and finalization only
7. a. No
b. v
8. a. v
b. vi
9. true, false, false, true, true
10. a. H1 = wp(s, c Л Q) = wp(s, i<n Л t=xn) = i-1<n Л tx=xn = i≤n Л t=xn-1
H2 = wp(s, ~c Л H1) = wp(s, i≥n Л i≤n Л t=xn-1) = wp(s, i=n Л t=xn-1)
= i-1=n Л tx=xn-1 = i=n+1 Л t=xn-2
H3 = wp(s, ~c Л H2) = wp(s, i≥n Л i=n+1 Л t=xn-2) = wp(s, i=n+1 Л t=xn-2)
= i-1=n+1 Л tx=xn-2 = i=n+2 Л t=xn-3
Hk = wp(s, ~c Л Hk-1) = i=n+(k-1) Л t=xn-k = i=n+k-1 Л t=xn-k
b. (i≤n Л t=xn-1) V (in Л t=x2n-(1+i) )
c. Does (i=5 Л t=1 Л n=3) Þ wp(R, t=xn)?
(i=5 Л t=1 Л n=3) Þ ([(i≤n Л t=xn-1) V (i>n Л t=x2n-(1+i) )]
= [(5≤3 Л 1=x3-1) V (5>3 Л 1=x2(3)-(1+5) )]
= (5>3 Л 1=x0) = true)
Therefore, the program will terminate with post-condition t=xn.
11. Does term(f,P)?
If y=0 initially, the predicate y>0 is false and the loop terminates immediately. If
y>0 initially, consider the Method of Well Founded Sets with measure y:
i. the value of y decreases by 1 with each iteration of the loop via y := y-1.
ii. the value of y is bounded from below since when y becomes equal to 0, the
loop must terminate since y>0 becomes false.
iii. the value of y may assume only a finite number of values (y0, y0-1, y0-2, …, 0)
since it decreases by an integral amount (1) with each iteration of the loop.
Therefore, by the Method of Well-Founded Sets, term(f,P).
Does (y=0) Þ ( f = I )?
(y=0) Þ ( f = (z,y := z+x(0),0)
= (z,y := z,0) )
(y=0) Þ ( I = (z,y := z,0) ) √
Does (y≠0) Þ ( f = f o g )?
case a: Does (y<0) Þ ( f = f o g )?
(y<0) Þ ( f = undefined )
(y<0) Þ ( f o g = undefined o (z,y := z+x,y−1)
= undefined ) √
case b: Does (y>0) ÞÞ ( f = f o g )?
(y>0) Þ ( f = (z,y := z+xy,0) )
(y>0) Þ ( f o g = (z,y := z+xy,0) o (z,y := z+x,y−1)
= (z,y := (z+x)+x(y−1),0)
= (z,y := z+xy,0) )√
Therefore, f = [P].
12. a. qh(X) = ( f(X)=foh(X0) )
initialization function: h = [y := 1; z := N] = (y,z := 1,N) (by observation)
while loop function: f = (z≥0 -> z,y := 0,yz!) (by observation)
X f(X) foh(X0)
------
z 0 0
y yz! (1)N!
Setting f(X)=foh(X0) yields:
0 = 0
yz! = N!
Therefore, q = ( y = N!/z! Л z≥0 )
b. I: y = N!/z! (Note that z≥0 is not required for weak correctness.)
INITIALIZATION: Does P => I?
P = (N≥0 Л y=1 Л z=N) => y = 1
=> N!/z! = z!/z! = 1 √
PRESERVATION: Does {I Л b} s {I}?
I Л b = y=N!/z! Л z≠0
{ y=N!/z! Л z≠0 }
y := y*z
{ y=zN!/z! Л z≠0 } = { y=N!/(z-1)! Л z≠0 }
z := z−1
{ y=N!/((z+1)-1)! Л z+1≠0 } = { y=N!/z! Л z+1≠0 } Þ I √
FINALIZATION: Does (I Л ~b) => Q?
(I Л ¬b) = (y=N!/z! Л z=0) = (z=0 Л y=N!) = Q √
13. false, true, false, false, false