Differences
This shows you the differences between two versions of the page.
Next revision | Previous revision | ||
sav08:language_with_dynamic_allocation [2008/04/08 17:40] vkuncak created |
sav08:language_with_dynamic_allocation [2008/04/08 23:22] vkuncak |
||
---|---|---|---|
Line 2: | Line 2: | ||
Recall syntax of [[Simple Programming Language]]. | Recall syntax of [[Simple Programming Language]]. | ||
+ | |||
+ | In addition to | ||
+ | x = T | ||
+ | if (F) c1 else c2 | ||
+ | c1 ; c2 | ||
+ | while (F) c1 | ||
+ | we have new basic statement: | ||
+ | x.f = e | ||
+ | x = new | ||
+ | In expressions we use | ||
+ | x.f | ||
+ | for dereferencing. | ||
+ | |||
+ | Resulting syntax: | ||
+ | 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 ::= V | null | T.f | ||
+ | F ::= (T=T) | (~F) | (F & F) | (F|F) | ||
+ | V ::= x | y | z | ... | ||
+ |