Formal Specification in Z

• Z Specification
  • Types (optional) - Generic and enumerated types for data manipulated by the system
  • Constants (optional) - Elements that aren’t changed by the system and their types
  • State space - System variables, their types and invariants about relationships between system elements
  • Initial (optional) - Set of formulas to describe the possible initial states
  • Operations - Describes the possible steps from a state to another state via a set of formulas in an operation
    • Preconditions - Formulas about the current variable values
    • Postconditions - Formulas about the variable values in the next state
• Schema - group together (and then later reuse) related information
• State Space Schema - Describes possible states, state is a set of variables with their types
• ”?” - used to represent input
  • p? is an input
• ”!” - used to represent output
  • q! is an output
• Local Variable - Variable that appears in the signature of an operation without a ”?” or ”!”
• A function f from set A to set B is surjective if every element of B is matched with some element of the domain of f