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)
\]
State variable
, which denotes a function, is assigned an updated version of this function.
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.