Type-Structure Abstractions

D ::= ...| var I:T | class I=T
T ::= newint | I

• Class = type-structure abstraction.
  • type I=T

class M = newint
var A:M; var B:M;
var C:newint
in A:=0; B:=@A+@C

• A and B bind to distinct locations!
• Body of M is evaluated each time it is invoked.
• Lazy evaluation of type abstractions.
• Copy rule applies:
  • var A: newint; var B: newint;
    var C:newint
    in A:=0; B:=@A+@C