Differences

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

--- sav08:semantics_of_dynamic_object_allocation [2008/04/08 16:46]
vkuncak created
+++ sav08:semantics_of_dynamic_object_allocation [2008/04/08 23:28]
vkuncak
@@ Line 1: / Line 1: @@
 ====== Semantics of Dynamic Object Allocation ======
+ x = new()
+Example program we wish we can prove:
+   x = new();
+   y = new();
+   assert (x != y);
+Also:
+  assume (ALL n. next n != x);
+  y = new();
+  assert (ALL n. next n != x);
+Solution:
+++++|
+  x = new();
+Becomes:
+  assume (t notin S);
+  x := t;
+  S = S U {t};
+++++
+We obtain formulas with sets, in FOL eliminate them using quantifiers.