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:34] 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. | ||