Assignment #7 + Solution Winter 2009

209 views8 pages
Published on 16 Oct 2011
School
University of Waterloo
Department
Computer Science
Course
CS245
Professor
CS 245 Winter 2009
Assignment 7
Due: Thu 26 Mar 2009 10am in the CS245 Drop Boxes
40 marks
SOLUTION SET
There may be multiple correct answers to this question.
1. (40 marks) For each of the following programs, if the program satisﬁes its speciﬁcation for
partial correctness, use program correctness techniques to show it is correct. State any loop
invariants. Use natural deduction (without transformational proof rules for propositional
and predicate logic) to prove any veriﬁcation conditions. If the program does not satisfy its
speciﬁcation, provide a counterexample and demonstrate that your counterexample does not
satisfy the speciﬁcation.
1
Unlock document

This preview shows pages 1-3 of the document.
Unlock all 8 pages and 3 million more documents.

(a) (18 marks)
(|true |)
x = 2 * x;
if (y >= 0) {
if (y=0) {
y = x + y;
}else {
y = 2 * y;
}
}else {
y = x + 2;
}
(| wy= 2w|)
Annotated Program:
(|true |)
x = 2 * x;
(| wx= 2w|) Derived Asn (VC 1)
if (y >= 0) {
(|(wx= 2w)(y>0) |) If-then-else
if (y=0) {
(|(wx= 2w)(y>0) (y= 0) |) If-then-else
(| wx+y= 2w|) Implied (VC 2)
y = x + y;
(| wy= 2w|)
}else {
(|(wx= 2w)(y>0) ∧ ¬(y= 0) |) If-then-else
(| w2y= 2w|) Implied (VC 3)
y = 2 * y;
(| wy= 2w|) Asn
}
(| wy= 2w|)
}else {
(|(wx= 2w)∧ ¬(y>0) |) If-then-else
(| wx+ 2 = 2w|) Implied (VC 4)
y = x + 2;
(| wy= 2w|) Asn
}
(| wy= 2w|) If-then-else
Unlock document

This preview shows pages 1-3 of the document.
Unlock all 8 pages and 3 million more documents.

VC 1: w2x= 2w
1. 2x= 2x= I
2. w2x= 2wI 1
VC 2: (wx= 2w)y>0y= 0 wx+y= 2w
1. (wx= 2w)y>0y= 0 premise
2. wx= 2wE 1
3. y= 0 E 1
4. w0x= 2w0assumption
5. x+ 0 = 2w0algebra 4
6. x+y= 2w0=E 3
7. wx+y= 2wI 6
8. wx+y= 2wE 2,47
VC 3: (wx= 2w)y>0y6= 0 w2y= 2w
1. (wx= 2w)y>0y6= 0 premise
2. 2y= 2y= I
3. w2y= 2w
VC 4: (wx= 2w)∧ ¬(y>0) wx+ 2 = 2w
1. (wx= 2w)∧ ¬(y>0) premise
2. wx= 2wE 1
3. w0x= 2w0assumption
4. x+ 2 = 2w0+ 2 algebra 3
5. x+ 2 = 2(w0+ 1) algebra 4
6. wx+ 2 = 2wI 5
7. wx+ 2 = 2wI 5
Unlock document

This preview shows pages 1-3 of the document.
Unlock all 8 pages and 3 million more documents.