This is an old revision of the document!
Language with Specified Procedures
Program is a collection of procedures.
Global and local variables.
New statement: procedure call.
x = p(x1,...,xN)
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 }