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:30]
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 (x1 notin S);
+  x := x1;
+  S = S U {x1};
+for fresh variable x1.
+++++
+We obtain formulas with sets, in FOL eliminate them using quantifiers.