State and operations

Z


  • $state == [ decls | constraints ]$
  • $op == [ %D state; decls | constraints ]$

Change and invariance

  • $ %D state == state /\ state' $
  • $ %X state == state = state' $

Verification
  • $ state /\ pre( op ) => op $
slide: Model-based specification