Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Last revision Both sides next revision | ||
sav08:semantics_of_dynamic_object_allocation [2008/04/09 16:10] ersoy |
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: ++++| |