Formal Specification

Intro

• 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.

Proposition

• 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.

Predicate

• 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.

Powerset

• 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.