Homework # 1
due January 30

Reading

Please read Appendix A in your textbook.

Problems

• Suppose we are doing an analysis in which we determine at each program point whether the following two facts is true or false or unknown: $x=0$, $x=1$. Suppose we wish to preserve as much information as possible about these facts. Draw the entire lattice. Indicate what the bottom $\bot$ and $\top$ values are.
• Do the same for the two facts $y=0$, $z=0$. Why is there a difference?
• The proof of Lemma A.2 is too concise. It doesn't convince the reader that the (A.1) is actually a lower bound. (``Clearly'' is not clear to me). Give a proof that (A.1) is indeed a lower bound of $Y$.
• On page 396, the authors assert that the monotone function space is a complete lattice if the input lattices are complete lattices. Prove this result. In particular, you must prove that the definition of $\bigsqcup Y$ actually results in a monotone function.
• Come up with an example lattice and a monotone function for which is not the least fixed point of $f$.
• Can you come up with an example for which $f$ is affine? Why not?

Submission

As with all homeworks, please turn in your homework on paper at the beginning of lecture.

About this document