Program is a collection of procedures.

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)

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 }