# Formal Specification

From Suhrid.net Wiki

Jump to navigationJump to search## Contents

# 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. - The state schema
**defines the set of valid states**which the system may assume.

## Operations

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

### Delta

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

### Xi

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