Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
sav08:language_with_dynamic_allocation [2008/04/08 20:09] vkuncak |
sav08:language_with_dynamic_allocation [2008/04/08 20:57] vkuncak |
||
---|---|---|---|
Line 16: | Line 16: | ||
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 | |
+ | assert(F) | assume(F) | havoc x | | ||
+ | (if (F) c else c) | c ; c | (while (F) c) | ||
T ::= K | V | T.f | | T ::= K | V | T.f | | ||
F ::= (T=T) | (~F) | (F & F) | (F|F) | F ::= (T=T) | (~F) | (F & F) | (F|F) |