Differences

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

--- sav08:language_with_specified_procedures [2008/04/09 00:32]
vkuncak created
+++ sav08:language_with_specified_procedures [2008/04/09 10:19]
vkuncak
@@ Line 9: / Line 9: @@
 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:Obj,...,xn:Obj) : Obj
+        requires F
+        ensures F
+        { c; return T }