Program is a collection of procedures.

Global and local variables.

New statement: procedure call.

x = p(x1,...,xN)

For each procedure precondition and postcondition.