State and operations

Z

       
semantic model object-oriented
abstraction structural behavioral
inheritance subtypes subclasses

Change and invariance

  • ∆state ≡ state ∧state′
  • Ξstate ≡ state = state′

Verification
  • ∆state ≡ state ∧state′
  • Ξstate ≡ state = state′
slide: Model-based specification