• Invariants different from pre/post-conditions
  • Resulting program invariants hold at every program point
  • Uses pack/unpack commands, but good defaults can be constructed for these
  • No linear type system
  • Components are not unique references—objects (pointers) can freely be copied
  • Fields can freely be read
  • No additional features of abstraction needed to support the specification of modifications
  • Sound