LARA

Semantics of Field Reads and Writes

How to model $x.f$ ?

How to model field assignment $x.f=y$ ?