This is an old revision of the document!
Semantics of Field Reads and Writes
How to model field assignment ?
What about null pointer checks?
Examples:
y = x.next.next x.next.next.prev = y (x = null | x.next == y)
Statement simplification.
Short-circuit evaluation.
Type and definition sketch of a recursive (Scala) function that simplifies expressions and statements.