Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
sav08:semantics_of_dynamic_object_allocation [2008/04/08 23:30] vkuncak |
sav08:semantics_of_dynamic_object_allocation [2009/03/18 10:47] vkuncak |
||
---|---|---|---|
Line 9: | Line 9: | ||
Also: | Also: | ||
- | assume (ALL n. next n != x); | + | assume (ALL n. (n : alloc --> next n != x)); |
y = new(); | y = new(); | ||
- | assert (ALL n. next n != x); | + | assume (ALL n. (n : alloc --> next n != x)); |
Solution: ++++| | Solution: ++++| | ||
Line 17: | Line 17: | ||
Becomes: | Becomes: | ||
assume (x1 notin S); | assume (x1 notin S); | ||
- | x := x1; | + | x = x1; |
S = S U {x1}; | S = S U {x1}; | ||
for fresh variable x1. | for fresh variable x1. | ||
++++ | ++++ | ||
- | We obtain formulas with sets, in FOL eliminate them using quantifiers. | + | We obtain formulas with sets, in FOL eliminate them using quantifiers as in [[Deciding a language of sets and relations]]. |