[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [Samples] / comp.spec.Z
[Index] [Contents] [Source Text] [About] [Notation] [Copyright] [Comment/Contact] [Search ]
Wed Jun 8 13:52:30 PDT 2011

Contents


    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

      Special Symbols used in Z Specifications

      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