Homework Assignments

Please check the course syllabus for our late submission policy.
Instructions on how to submit programming assignments electronically can be found here.

All files below are in either html or PDF format.

Assignments

• Homework 1
• Homework 2 (you will also need the file hw2-sml).
  Here are some test cases for the homework.
• Homework 3
• Homework 4
• Homework 5 (you will also need the file hw5-sml).
• Homework 6

Solutions

• Homework 1
• Homework 2
• Homework 3
• Homework 4
• Homework 6

Exercises

1. Ex. 2.7 from the textbook.
2. Ex. 3.5 and 3.6 from the textbook.
3. Ex. 3.5, 3.6, and 3.8(1) from the textbook.
4. Ex. 4.4 from the textbook.
5. Complete the proof of Prop. 4.7 in the textbook by proving the missing cases.
6. Show by structural induction on arithmetic expressions that the relation A[[a]], as defined in the textbook, is a total function for all arithmetic expressions a.
7. Show by structural induction on Boolean expressions that the relation B[[b]], as defined in the textbook, is a total function for all Boolean expressions b.
8. Complete the proof seen in class of Lemma 5.4 by proving the missing cases.
9. Use the your completed proof of Lemma 5.4 as a model to prove Lemma 5.3.
10. Complete the proof seen in class of Theorem 5.7 by proving the missing cases.
11. Ex. 5.10 and 5.12(ii) from the textbook.
12. Redo Problem 4 in Homework 3, but this time use structural induction, in both point a and b.
13. Ex. 8.2 and 8.7 from the textbook.
14. Consider any partial order and let X be a set of elements of the p.o. Prove that if X has a lub, this lub is unique.
15. Let X = {b0, b1, ...} be an infinite set and consider the cpo (Pow(X), <=) where <= is the subset relation. Let f:(Pow(X), <=) -> (Pow(X), <=) be the function defined as follows:
    - f(Y) = {b0} if Y is finite
    - f(Y) = {b0, b1} if Y is infinite.
    Show that f is monotonic but is not continuous.
16. Let (S', <=) be the cpo defined in Problem 2.3 of Homework 4. Define a function f:(S', <=) --> (S', <=) that is not continuous.
17. Prove that the finite product with k cpos with bottom is a cpo with bottom.
18. Prove that the projection function pi_i from a product cpo to the i-th component cpo is continuous.
19. Prove Proposition 9.2 in the textbook.
20. Prove Lemma 9.4 in the textbook.
21. Ex. 6.6 and 6.15 from the textbook.
22. Extend the set of Hoare rules in order to provide appropriate axiomatic semantics for the command "unless b do c" seen in Homework 4.
23. Prove the following partial correctness assertion { true } R := X; Q := 0; while Y <= R do (R := R-Y; Q := Q+1) { X = (Q x Y) + R   /\  R < Y}