Z (pronouned Zed!) is a specification language that works at a a high level
of abstraction so that even complex behaviors can be described precisely
and concisely. The Semantics of Z is matheamtical and so formulae can be
manipulated algebraically and logically.
Its purpose is to make it easy to specify highlevel functional requirements
using mathematical notation.
(ZRM): The best online source of definitive information on Z was
Spivey 89, J M Spivey,
the Z Notation Reference Manual, PHI 1989.
Much of the following is my own translation and interpretation of
this work. You can find links to a free online (but copyrighted) version
at
[Spivey01]
in my bibliography.
More recently there is an ISO Standard for the Z notation that you may need to consult.
- abstraction_schema::=` In data refinement a schema that documents the relationship between abstract and concrete
state spaces`.
- basic_type::=A named type denoting a set of objects regarded as atomic in a specification.
- binding::=an object with one or more components named by identifiers. An element of a schema type.
- cartesian_product_type::=a type containg n-tuples of objects drawn from other type.
- constraint::=a property that values of variables must satisfy to fit a decalration.
- data_refinement::=`the process of showing that one set of operations is implementd by another set on a different
state space`.
- derived_component::=`A component of a schema describing the state space of an abstract data type whose value can
be deduced from values of the othe components`.
- extension::@(situation,situation)=/restriction.
- finitary::=??.
- graph::=the set of ordered pairs of objects that satisfy a binary relation.
- implicit_pre_condition::=`A precondition that is not explicitly stated in a specification but is implicitly part of the
post_condition or of the invariant of the final state`.
- join::=`two typecompatible signatures can be joined to forma a signature that has all variables of both the original
ones paired with the same types`.
- logically_equivalent::@(predicates,predicates)=`expressing the same property, that is when they are true in exactly
the same conditions`.
- loose_specification::=`a spcification where the values of the global variables are not completely determined by the
predicates that constrain them`.
- non_deterministic::=`an operation in an abstract data type where there may be more than one possible state after for
each single state befor it`.
- operation_refinement::=`the process of showing that one operation is implemented by another with the same state
space`.
- pre_condition::=`the condition on a state before an operation and on its inputs that there should exist a possible state
afterwards and outputs satisfying its post_condition`.
- predicate::=a formula describing a relationship between values of the variables in a signature.
- prperty::=` the mathematical relationship expresses by a predicate characterized by the situations in which the
predicate is true`.
- restriction::@(situation,situation)=` signature(2nd) is a subsignature (1st) and each variable in signature(2nd) has the
same value as it has in the (1st) signature`.
- relation::=??.
- schema_type::=a type contain bindings with name components drawn from other types.
- scope_rules::=rules that determine what identifiers may be used at each point in a specification and what definition each identifier refers to.
- sequential_composition::operation.syntax><operation.syntax->operation.syntax= (1st) bold_semicolon (2nd).
- sequential_composition::=the operation where (1st) occurs imediatly before (2nd).
- set_type::types->types=the sets of objects of type (_).
- signature::variables<>->type.
- situation::=that which determines the values of variables in a signature.
- state_space::=the set of possible states.
- sub_signature::@(signature,signature)=(==>).
(types) type>=={basic_type, set_type, cartesian_product_type, schema_type).
- type::=used to determine the set of values that an expression can take.
. . . . . . . . . ( end of section Z Glossary) <<Contents | End>>
Z depends on the being able to express mathematical style formulae. As a result it is either hand written or prepared using TeX and a special font.
There is a computerized code developed at York University England and tools that translate that into TeX. A goal for my MATHS project is to get the power of Z without the baggage of TeX.
There are my notes on TeX:
[ comp.text.TeX.html ]
Also see the Z Reference Manual(ZRM).
The syntax below uses the conventions from
[ comp.text.ASCII.html ]
,
[ math.lexicon.html ]
, and
[ math.syntax.html ]
Based on ZRM
- Specification::= L(Paragraph, EOLN).
- Paragraph::= "[" List(Ident) "]" | Box | Definition | Predicate.
- Definition::=Schema_Name O( Gen_Formals) Define_symbol Schema_exp | Def_Lhs "==" Expression | Ident "::=" L(Branch, "|").
- Box::= Axiomatic_Box | Schema_Box | Generic_Box.
- Define_symbol::=equals sign with circumflex accent.
- Axiomatic_box::= vertical_bar Decl_part Possible_Axioms.
- Possible_Axioms::=O( EOLN dividing_line EOLN vertical_bar Axiom_part).
| Decls
|-------
| Axioms
- Schema_Box::= dash Schema_Name O(Gen_Formals) long_dash EOLN vertical_bar Decl_Part Possible_Axioms.
-------Name----------
| Decls
|------------------------
| Axioms
- Generic_Box::= double_dash O(Gen_Formals) long_double_dash EOLN vertical_bar Decl_Part Possible_Axioms.
======Name======
| Decls
|------------------------
| Axioms
- Decl_Part::= L(Basic_Decl, Sep).
- Axiom_Part::=L(Predicate, Sep).
- Sep::= ";" | EOLN.
- Def_Lhs::= Var_name O(Gen_Formals) | Pre_Gen Ident | Ident In_Gen Ident.
- Branch::= Ident | Var_Name French_open_quotes Expression French_close_quotes.
- Schema_Exp::= (for_all | for_some | for_one ) Schema_text big_dot Schema_Exp | Schema_Exp_1.
- Schema_Exp_1::= "[" Schema_Text "]" | Schema_Ref | IBM_not Schema_Exp_1 | Schema_Exp_1 infix_operator Schema_Exp_1 | Schema_Exp_1 "\" "(" List(Decl_Name) ")" | "(" Schema_Exp ")"
- Infix::(infix_operator->${binding_power::Nat=1st, associativity::{left,right}=2nd. }=
(and+>(7, left) | or+>(6, left) | implies+>(5, right) | iff+>(4, left) | restriction+>(3, left) | back_slash+>(2, left) | semicolon+>(1, left)).
- Schema_Text::= Declaration O(bar Predicate).
- Schema_ref::= Schema_Name Decoration O(Gen_Actuals).
- Declaration::= L(Basci_Decl, ";").
- Basic_Decl::= List(Decl_name)":" Expression | Schema_ref.
- Predicate::= (for_all | for_some | for_one ) Schema_text big_dot Predicate | Predicate_1.
- Predicate_1::=L(Expression Rel) |Prefix_Rel Expression | Schema_Ref | "pre" Schema_ref | "true" | "false" IBM_not Predicate_1 | Predicate_1 infix_operator Predicate_1 | "(" Predicate ")".
- Rel::= "=" | ∈ | Infix_Rel.
- Expression_0::= λ Schema_Text big_dot Expression | μ Schema_Text O(big_dot Expression) | Expression.
- Expression::= Expression Infix_Gen Expression | L(Expression_1, cross) | Expression_1.
- Expression_1::= Expresssion Infix_Fun Expression | \powset Expression_3 | Prefix_Gen Expression_3 | minus Expression_3 | Expression_3 Postfix_Fun | Expression_3 superscript(Expression) | expression_3 left_barred_paren Expression_0 right_barred_paren | Expression_2.
- Expression2::= Expression_2 Expression_3 | Expression_3.
- Expression_3::= Var_Name O(Gen_Actuals) | Number | Schema_Ref | Set_Expresssion | left_diamond_bracket O(L(Expression)) right_diamond_bracket | left_double_bracket L(Expression) right_double_bracket | θ Schema_Name Decoration | Expression_3 "." Var_Name | left_paren Expression_0 right_paren.
- Set_Exp::= left_brace L(Expression) right_brace | left_brace Schem_Text O(big_dot Expression) right_brace.
- Ident::= Word Decoration.
- Decl_Name::= Ident | Op_name.
- Var_Name::= Ident | left_paren Op_Name right_paren.
- Op_name::= "_" Infix_Sym "_" | Prefix_Sym "_" | "_" Post_Sym | "_" left_barred_paren "_" right_barred_paren | "_".
- Infix_Sym::= Infix_Fun | Infix_Gen | Infix_Rel.
- Prefix_Sym::= Prefix_Gen | Prefix_Rel.
- Gen_Formals::= "[" List(Ident) "]".
- Gen_Actuals::= "[" List(Expression) "]".
- Word::@lexeme=undecorated name of special symbol.
- Stroke::@lexeme= "'" | "?" | " !" | subscript_digit.
- Infix_Fun::@lexeme=Infix function symbol.
- Infix_Rel::@lexeme=Infix relation symbol.
- Infix_Gen::@lexeme=Infix generic symbol.
- Prefix_Gen::@lexeme=prefix generic symbol.
- Prefix_Rel::@lexeme=prefix relation symbol.
- Postfix_Fun::@lexeme=postfix function symbol.
- Number::=unsigned decimal integer.
. . . . . . . . . ( end of section Z Syntax) <<Contents | End>>
Source:
[Spivey88]
.Road-Works-Ahead
In terms of MATHS, A Z schema with signature S and predicate P is easily
mapped into an equivalent Net. S is made up of
declarations like v:T. Declarations of form v:T become v::T.
and are then placed between between ".Net" and ".Close.Net"(laid out)
or "Net{" and "}"(inline). The Ps are translated
and place inside the Net as well.
Similarly most Z definitions become MATHS definitions.
.TBA
. . . . . . . . . ( end of section Z Semantics) <<Contents | End>>
Bibliography
%20Z%20
Usenet newsgroup:
comp.specification.z
EMail archive: archive-server@comlab.ox.ak.uk
[ topics ]
(Google groups).
. . . . . . . . . ( end of section Z See Also) <<Contents | End>>