Formal Specification

From Wiki
Jump to navigationJump to search


  • A specification is a statement of requirements for a system, object or process.
  • A formal specification is one in which the language of mathematics is used to construct such a statement.
  • Z is a formal specification language based on set theory and logic.
  • In a Z specification, discrete mathematical structures are used to create a model of the required system.
  • Predicate logic is used to state precisely the required relationships between the mathematical structures, thus defining the set of possible valid states for the system.
  • The math structures are more abstract and problem oriented compared to the data structures used in programming languages.
  • Predicate logic is then used to precisely define the required effect of operations in the system.
  • Philosophy is to specify what each operation is supposed to do and not how to do it.


  • A proposition is a statement which is either true or false, but not both.
  • e.g. 5 < 10 is a proposition, but not x > 0.


  • Z is a typed language, to introduce a variable in a specification, it needs to be declared and associated.
  • e.g. x : N, where N is set of all natural numbers.
  • A predicate is an expression containing one or more free variables which act as a placeholders for values drawn from specific sets.
  • e.g. give x, y : N, the expression x = y + 3 is a predicate with two free variables x and y.
  • A predicate is a template for constructing propositions by plugging in values.
  • A predicate is like a proposition with various "slots" to be filled in by objects of various kinds.
  • Therefore to build a proposition from a predicate, we must remove all the free variables.
  • This can be done either by:
    • Replace free variable with a particular value.
    • Bind it with a quantification.

∀ <name> : <type> | <optional constraint> ∙ <predicate>

| means "such that" and ∙ "it is true that"

Sets and Types

  • Every expression in Z belongs to a set called its type.
  • For every variable, its type must be declared.
  • We can introduce our basic types or given sets by typing the name of the type within squared brackets:
    • [PERSON] . (Note no indication as to how persons are represented.)
  • Another way is by listing the names of the elements of the type in a free type definition. For example,
    • COLOUR ::= red | green | blue, FUEL ::= petrol | diesel | electricity

Describing Sets

  • A set can be described in extension, enumerating all elements in curly brackets.
  • e.g. numset == {4,5,6,7,8,9}
  • Can also be described using set comprehension:
  • e.g set == {declaration | predicate ∙ expression }
    • where declaration has 1 or more bound variables.
    • predicate constrains the values of bound variables.
    • expression gives the form of the elements of set
  • e.g. numset == { n : Z | n ≥ 4 ∧ n ≤ 9 ∙ n}

Note, if only 1 variable in declaration and expression is that variable, then expression can be omitted.

  • e.g. numset == { n : Z | n ≥ 4 ∧ n ≤ 9 }
  • Predicate may be omitted, if it is always true.


  • The powerset of a set S, is the set of all subsets of S.
  • The size of powerset is 2^size(s).

Structure of a Z specification

  • A Z specification involves creating a model of the required system.
  • The structure/state of the system is represented using sets and the relationships between elements of the state are expressed using the language of logic.
  • Logic is then used to specify operations to change/make queries about the state of the system.

System state

  • An axiomatic description is a Z construct for defining a global variable which remains in scope throughout the specification.
  • Top half of the axiomatic description is a declaration and the bottom half is an optional predicate specifying a constraint on the value of the declared variable.
  • Use sets to specify the state.
  • Use predicates to specify state invariants about the system.
  • In Z the declaration of the sets along with the predicates constraining their values is called a schema.
  • Top half contains declarations - state variables and bottom half contains the state invariants.
  • All predicates are implicitly and-ed together.
  • The state schema defines the set of valid states which the system may assume.


  • The system may move from one valid state to another by operations which change the values of one or more of the state variables.
  • Input identifiers terminated with ? and Output identifiers terminated by !.
  • State variables need to be referred to the before and after state when an operation takes place.
  • Before variables are undecorated.
  • After variables are terminated with a '.
  • Preconditions: Predicates which state what must be true about the before state of the system and the inputs in order for the operations to take place.
  • Postconditions: Predicates which relate the before state and inputs to the after state and outputs.
  • All declarations and predicates are local to the schema and not available in other schema, so the operation must use the delta notation to indicate which schema it is modifying.


  • The delta will bring into scope the before and after versions of the state variables and invariant predicates.
  • Otherwise each before and after variable state as well before and after versions of predicates need to be explicitly specified.


  • Inclduing 𝛯S in an operation schema, where S is a state makes visible before and after version of declarations and predicates together with the assertion that these variables are not changed by the operation.
  • Used for operations which dont change the state.

Schema Combination

  • Two schemas S and T can be combined using and, or, implies, equivalence operators.
  • This defines a schema which merges declarations and gives a predicate which is combined using the schema combination operator specified above.
  • S3 ≙ S1 ∧ S2

Initial State

  • Initial state is a special after state without a corresponding before state.
  • The state is suffixed with a ' mark in the schema declaration.
  • All state variables are decorated with a ' mark.