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.