Changes between Version 4 and Version 5 of MemoryAnalysis

Timestamp:

02/18/16 15:14:09 (10 years ago)

Author:

zmanchun

Comment:

--

MemoryAnalysis

@@ -77 +77 @@
     `sub((T)e)={e}`
 
+==== statements ====
+
+1. assignment: `l := e`
+   `impact(l := e) = impact(l) U impact(e)`;
+
+2. call: `l := f(e0, e1, e2, ...)`
+ * f is atomic specified (`$atomic_f`) and f has contracts: \\
+   **TBC**
+ * otherwise:\\
+   `impact(l := f(e0, e1, e2, ...)) = impact(l) U impact(e0) U impact(e1) ...`
+
+3. guarded statement: `[e]s`
+    `impact([e]s) = impact(e) U impact(s)`
+
+
+ 
 
 
 
 
-
-