Differences

This shows you the differences between two versions of the page.

--- sav08:semantics_of_field_reads_and_writes [2008/04/08 17:23]
vkuncak created
+++ sav08:semantics_of_field_reads_and_writes [2008/04/08 23:38]
vkuncak
@@ Line 1: / Line 1: @@
 ====== Semantics of Field Reads and Writes ======
-What is
+How to model $x.f$ ? ++|term $f(x)$++
-  x = y.f;
-  x.f = y;
-Function associated with list, function update.
+How to model field assignment $x.f=y$ ?
+++++|
+Use function update construct:
+\[
+    f = f(x:=y)
+\]
+State variable $f$, which denotes a function, is assigned an updated version of this function.
+++++
-Null pointer checks.
+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.