Differences
This shows you the differences between two versions of the page.
Next revision Both sides next revision | |||
sav08:language_with_specified_procedures [2008/04/09 00:32] vkuncak created |
sav08:language_with_specified_procedures [2008/04/09 00:35] vkuncak |
||
---|---|---|---|
Line 9: | Line 9: | ||
For each procedure precondition and postcondition. | For each procedure precondition and postcondition. | ||
+ | |||
+ | Syntax summary: | ||
+ | |||
+ | c ::= x=T | x.f=T | x=new | x=P(x1,...,xN) | ||
+ | assert(F) | assume(F) | havoc x | | ||
+ | (if (F) c else c) | c ; c | (while (F) c) | ||
+ | D ::= proc P(x1,...,xn) | ||
+ | requires F | ||
+ | ensures F | ||
+ | { c; return T } | ||