Revision as of 11:26, 2 February 2012

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.

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"

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

@@ Line 34: / Line 34: @@
 = 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