Assignment #7 + Solution Winter 2009

209 views8 pages
user avatar
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 satisfies its specification 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 verification conditions. If the program does not satisfy its
specification, provide a counterexample and demonstrate that your counterexample does not
satisfy the specification.
1
Unlock document

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

Already have an account? Log in
(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.

Already have an account? Log in
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.

Already have an account? Log in

Document Summary

Due: thu 26 mar 2009 10am in the cs245 drop boxes. There may be multiple correct answers to this question: (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. 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 (a) (18 marks) (| true |) x = 2 * x; if (y >= 0) { if (y=0) { y = x + y; } else { y = 2 * y; } else { y = x + 2; (| w y = 2w |) Annotated program: (| true |) x = 2 * x; (| w x = 2w |)