Formal Specification

From Suhrid.net Wiki
Jump to navigationJump to search

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.