Declaration Abstractions

D ::= ...| module I={D} | import I

• Module = abstraction of declarations.
• Module invocation = import.

module M = { class K = newint; var A: K;
    proc P = A:=0 };
var B: newint;
import M
in call P; B:=@A

Declarations in M is not visible in program until M is imported.