Lecture preparation

Before lecture, read the paper assigned below, and submit two items to the submission website:

Also keep in mind that you will need to write a paper summary for your choice of papers throughout the semester.


Read the paper Separation Logic by Peter O'Hearn.

Why are we reading this paper?

What to learn from this paper?

Answer this question

Suppose we made the tree (described on p91, middle column) share nodes whenever an inserted tree matched one already present, saving memory by storing a pointer to the existing tree. With such an implementation what does tree(tau_1, root_1) * tree(tau_2, root_2) mean? Does modifying root_1 affect just tau_1 (as before), or also tau_2?