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 [2009/05/26 12:42]
vkuncak
@@ Line 3: / Line 3: @@
 Program is a collection of procedures.
-Global and local variables.
+Two kinds of variables:
+  * global variables, visible and modifiable by all procedures
+  * local variables, for each procedure
 New statement: procedure call.
   x = p(x1,...,xN)
-For each procedure precondition and postcondition.
+Each procedure has its
+  * precondition
+  * 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 }