Sharing of Modules

module S = { var A: K;
    fun F=@A+1 };
module M = { import S; proc INIT=A:=0 };
module N = { import S; proc SUCC=A:=F };
in call M.INIT; call N.SUCC

• S is shared by M and N.
• Same A is altered by M and N.
• Eager evaluation of S essential.