This is an old revision of the document!
Semantics of Field Reads and Writes
How to model ? term
How to model field assignment ?
Use function update construct:
\[
f := f(x:=y)
\]
What about null pointer checks?
Examples:
y = x.next.next
x.next.next.prev = y
(x = null | x.next == y)
Statement simplification.