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,...,xn)
      requires F 
      ensures F
      { c; return T }