Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:language_with_dynamic_allocation [2008/04/08 20:09] vkuncak |
sav08:language_with_dynamic_allocation [2008/04/08 23:22] vkuncak |
||
|---|---|---|---|
| Line 11: | Line 11: | ||
| x.f = e | x.f = e | ||
| x = new | x = new | ||
| - | In expressions we expression | + | In expressions we use |
| x.f | x.f | ||
| for dereferencing. | for dereferencing. | ||
| Resulting syntax: | Resulting syntax: | ||
| - | c ::= x=T | x.f=T | x=new | (if (F) c else c) | c ; c | (while (F) c) | + | c ::= x=T | x.f=T | x=new | |
| - | T ::= K | V | T.f | | + | assert(F) | assume(F) | havoc x | |
| + | (if (F) c else c) | c ; c | (while (F) c) | ||
| + | T ::= V | null | T.f | ||
| F ::= (T=T) | (~F) | (F & F) | (F|F) | F ::= (T=T) | (~F) | (F & F) | (F|F) | ||
| V ::= x | y | z | ... | V ::= x | y | z | ... | ||
| - | K ::= 0 | 1 | 2 | ... | ||