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.