Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:language_with_specified_procedures [2008/04/09 00:35] vkuncak |
sav08:language_with_specified_procedures [2009/05/26 12:42] vkuncak |
||
|---|---|---|---|
| Line 3: | Line 3: | ||
| Program is a collection of procedures. | 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. | New statement: procedure call. | ||
| x = p(x1,...,xN) | x = p(x1,...,xN) | ||
| - | For each procedure precondition and postcondition. | + | Each procedure has its |
| + | * precondition | ||
| + | * postcondition | ||
| Syntax summary: | Syntax summary: | ||
| Line 15: | 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) | ||
| - | 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 } | ||