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