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.
Definition and type of a (Scala) function that simplifies expressions and statements.