Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Last revision Both sides next revision | ||
sav08:language_with_specified_procedures [2008/04/09 00:35] vkuncak |
sav08:language_with_specified_procedures [2008/04/09 10:19] vkuncak |
||
---|---|---|---|
Line 15: | Line 15: | ||
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) | ||
- | D ::= proc P(x1,...,xn) | + | D ::= proc P(x1:Obj,...,xn:Obj) : Obj |
requires F | requires F | ||
ensures F | ensures F | ||
{ c; return T } | { c; return T } | ||