LARA Semantics of Field Reads and Writes How to model ? term How to model field assignment ? Use function update construct: State variable , which denotes a function, is assigned an updated version of this function.
? 
?
, which denotes a function, is assigned an updated version of this function.