Contents

• The Z Formal Specification Language
• : Introduction
• : The Z Reference Manual
• : Z Standards
• : Z Glossary
• : Lexicon
• : Symbols used in Z
• : Z Syntax
• : : MATHS syntax
• : Z Semantics
• : Z See Also
• : : Books and Papers

The Z Formal Specification Language

Introduction

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.

The Z Reference Manual


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

Z Standards

More recently there is an ISO Standard for the Z notation that you may need to consult.

Z Glossary

1. abstraction_schema::=` In data refinement a schema that documents the relationship between abstract and concrete state spaces`.
2. basic_type::=A named type denoting a set of objects regarded as atomic in a specification.
3. binding::=an object with one or more components named by identifiers. An element of a schema type.
4. cartesian_product_type::=a type containg n-tuples of objects drawn from other type.
5. constraint::=a property that values of variables must satisfy to fit a decalration.
6. data_refinement::=`the process of showing that one set of operations is implementd by another set on a different state space`.
7. 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`.
8. extension::@(situation,situation)=/restriction.
9. finitary::=??.
10. graph::=the set of ordered pairs of objects that satisfy a binary relation.
11. 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`.
12. 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`.
13. logically_equivalent::@(predicates,predicates)=`expressing the same property, that is when they are true in exactly the same conditions`.
14. loose_specification::=`a spcification where the values of the global variables are not completely determined by the predicates that constrain them`.
15. 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`.
16. operation_refinement::=`the process of showing that one operation is implemented by another with the same state space`.
17. 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`.
18. predicate::=a formula describing a relationship between values of the variables in a signature.
19. prperty::=` the mathematical relationship expresses by a predicate characterized by the situations in which the predicate is true`.
20. 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`.
21. relation::=??.
22. schema_type::=a type contain bindings with name components drawn from other types.
23. scope_rules::=rules that determine what identifiers may be used at each point in a specification and what definition each identifier refers to.
24. sequential_composition::operation.syntax><operation.syntax->operation.syntax= (1st) bold_semicolon (2nd).
25. sequential_composition::=the operation where (1st) occurs imediatly before (2nd).
26. set_type::types->types=the sets of objects of type (_).
27. signature::variables<>->type.
28. situation::=that which determines the values of variables in a signature.
29. state_space::=the set of possible states.
30. sub_signature::@(signature,signature)=(==>). (types) type>=={basic_type, set_type, cartesian_product_type, schema_type).
31. type::=used to determine the set of values that an expression can take.

. . . . . . . . . ( end of section Z Glossary) <<Contents | End>>

Lexicon

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.

Symbols used in Z



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 ]

Z Syntax

Also see the Z Reference Manual(ZRM).

MATHS syntax

The syntax below uses the conventions from [ comp.text.ASCII.html ] , [ math.lexicon.html ] , and [ math.syntax.html ]

Based on ZRM

1. Specification::= L(Paragraph, EOLN).
2. Paragraph::= "[" List(Ident) "]" | Box | Definition | Predicate.

3. Definition::=Schema_Name O( Gen_Formals) Define_symbol Schema_exp | Def_Lhs "==" Expression | Ident "::=" L(Branch, "|").

4. Box::= Axiomatic_Box | Schema_Box | Generic_Box.
5. Define_symbol::=equals sign with circumflex accent.

6. Axiomatic_box::= vertical_bar Decl_part Possible_Axioms.
7. Possible_Axioms::=O( EOLN dividing_line EOLN vertical_bar Axiom_part).

    | Decls

    |-------

    | Axioms

8. Schema_Box::= dash Schema_Name O(Gen_Formals) long_dash EOLN vertical_bar Decl_Part Possible_Axioms.

    -------Name----------

    | Decls

    |------------------------

    | Axioms

9. Generic_Box::= double_dash O(Gen_Formals) long_double_dash EOLN vertical_bar Decl_Part Possible_Axioms.

    ======Name======

    | Decls

    |------------------------

    | Axioms

10. Decl_Part::= L(Basic_Decl, Sep).
11. Axiom_Part::=L(Predicate, Sep).
12. Sep::= ";" | EOLN.

13. Def_Lhs::= Var_name O(Gen_Formals) | Pre_Gen Ident | Ident In_Gen Ident.

14. Branch::= Ident | Var_Name French_open_quotes Expression French_close_quotes.

15. Schema_Exp::= (for_all | for_some | for_one ) Schema_text big_dot Schema_Exp | Schema_Exp_1.
16. 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 ")"
17. 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)).

18. Schema_Text::= Declaration O(bar Predicate).

19. Schema_ref::= Schema_Name Decoration O(Gen_Actuals).

20. Declaration::= L(Basci_Decl, ";").
21. Basic_Decl::= List(Decl_name)":" Expression | Schema_ref.

22. Predicate::= (for_all | for_some | for_one ) Schema_text big_dot Predicate | Predicate_1.

23. 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 ")".

24. Rel::= "=" | ∈ | Infix_Rel.

25. Expression_0::= λ Schema_Text big_dot Expression | μ Schema_Text O(big_dot Expression) | Expression.

26. Expression::= Expression Infix_Gen Expression | L(Expression_1, cross) | Expression_1.

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

28. Expression2::= Expression_2 Expression_3 | Expression_3.

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

30. Set_Exp::= left_brace L(Expression) right_brace | left_brace Schem_Text O(big_dot Expression) right_brace.

31. Ident::= Word Decoration.

32. Decl_Name::= Ident | Op_name.
33. Var_Name::= Ident | left_paren Op_Name right_paren.

34. Op_name::= "_" Infix_Sym "_" | Prefix_Sym "_" | "_" Post_Sym | "_" left_barred_paren "_" right_barred_paren | "_".

35. Infix_Sym::= Infix_Fun | Infix_Gen | Infix_Rel.
36. Prefix_Sym::= Prefix_Gen | Prefix_Rel.

37. Gen_Formals::= "[" List(Ident) "]".
38. Gen_Actuals::= "[" List(Expression) "]".

39. Word::@lexeme=undecorated name of special symbol.
40. Stroke::@lexeme= "'" | "?" | " !" | subscript_digit.
41. Infix_Fun::@lexeme=Infix function symbol.
42. Infix_Rel::@lexeme=Infix relation symbol.
43. Infix_Gen::@lexeme=Infix generic symbol.
44. Prefix_Gen::@lexeme=prefix generic symbol.
45. Prefix_Rel::@lexeme=prefix relation symbol.
46. Postfix_Fun::@lexeme=postfix function symbol.
47. Number::=unsigned decimal integer.

. . . . . . . . . ( end of section Z Syntax) <<Contents | End>>

Z Semantics

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

Z See Also

Books and Papers

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

. . . . . . . . . ( end of section Z) <<Contents | End>>

End