.Open 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. . The Z Reference Manual (ZRM): The best online source of definitive information on Z is Spivey 89, J M Spivey, the Z Notation, PHI 1989. .See ./zrm.pdf Much of the following is my own translation and interpretation of this work. .Open Z Glossary 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= (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`. .Close Z Glossary . 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 .Image Zsymbols2.GIF 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: .See http://www/dick/samples/comp.text.TeX.html .Open Z Syntax Also see the Z Reference Manual($ZRM). . MATHS syntax The syntax below uses the conventions from .See http://www/dick/samples/comp.text.ASCII.html , .See http://www/dick/samples/math.lexicon.html , and .See http://www/dick/samples/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). .As_is | Decls .As_is |------- .As_is | Axioms Schema_Box::= dash Schema_Name O(Gen_Formals) long_dash EOLN vertical_bar Decl_Part Possible_Axioms. .As_is -------Name---------- .As_is | Decls .As_is |------------------------ .As_is | Axioms Generic_Box::= double_dash O(Gen_Formals) long_double_dash EOLN vertical_bar Decl_Part Possible_Axioms. .As_is ======Name====== .As_is | Decls .As_is |------------------------ .As_is | Axioms .As_is 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 ::= "=" | \in | Infix_Rel. Expression_0::= \lambda Schema_Text big_dot Expression | \mu 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 | \theta 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`. .Close Z Syntax .Open Z Semantics .Source .See [Spivey88] .Road-Works-Ahead In terms of MATHS, A Z schema with signature S and predicate P is easily mapped into an equivalent Net. Declarations of form `v:T` become `v::T.` and are then placed between "Net{" and "}" along with the P. Similarly most Z definitions become MATHS definitions. .TBA .Close Z Semantics .Open Z See Also . Books and Papers Bibliography .Find %20Z%20 Usenet newsgroup: .See news:comp.specification.z EMail archive: archive-server@comlab.ox.ak.uk .Close Z See Also .Close Z