LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

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 | ...