Please use the alphabetical Index, Contents List, and your browsers search feature to find what you need.

This page generated at Thu Mar 4 08:29:52 PST 1999. This page is a sample piece of documentation generated from z.syntax.mth . For more information see the documentation on Dr. Botting's MATHS project.

Contents

    Syntax of The Formal Specification Language Z

    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/or a special font. The special fonts for MS Windows and Macintoshes and the TeX style. [ comp.text.TeX.html ] [ comp.text.ASCII.html ] [ math.syntax.html ]

    *New* Proposed standard lexemes for ASCII/EMail: [ z.lexis.html ]

    There is a computerized code developed at York University England and tools that translate that into TeX. A goal for Dr. Botting's MATHS project is to get the power of Z without the baggage of TeX. This notation is used in this document and is called MATHS.

    Grammar

    The following is based on Spivey 89
  1. Specification::= L(Paragraph, EOLN).
  2. Paragraph::= Declare_generic_sets| Box | Schema_Name O( Gen_Formals) Define_symbol Schema_exp | Def_Lhs == Expression | Ident "::=" L(Branch, "|") | Predicate.

  3. Declare_generic_sets::= "[" List(Ident) "]" .
  4. Box::= Axiomatic_Box | Schema_Box | Generic_Box.
  5. Define_symbol::=equals sign with circumflex accent.

  6. Axiomatic_box::= start_axiom Decl_part Possible_Axioms end_axiom.
  7. Possible_Axioms::=O( EOLN such_that EOLN Axiom_part).

    Email Form 

     	+..
     	  Decls
     	|--
     	  Axioms
     	-..
    It looks like this: 
    	| Decls
    	|-------
    	| Axioms

  8. Schema_Box::= start_schema Schema_Name O(Gen_Formals) dash EOLN Decl_Part Possible_Axioms end. Email Form 
     	+-- Name ---
     	  Decls
     	---
    giving 
    	 -------Name----------
    	| Decls
    	 --------------
    or 
     	+-- Name ---
     	  Decls
     	|--
     	  Axioms
     	---
    giving this kind of thing: 
    	 -------Name----------
    	| Decls
    	|--------------
    	| Axioms
    	 ----------------------
  9. Generic_Box::= start_generic O(Gen_Formals) double_dash EOLN vertical_bar Decl_Part Possible_Axioms.

    Email: 

     	+== [Para] ===
     	  Decls
     	|--
     	  Axioms
     	-==
    giving this kind of thing: 
    	 ======[Para]======
    	| 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_operator::= and| or| implies| iff| hide| rename| schema_compose. 
     Name    	EMail	TeX	MATHS
     and     	/\	\land	and
     or      	\/	\lor	or
     implies	==>	\implies
     iff    	<=>	\iff	iff
     hide   	|	\vbar
     rename 	\	?
     compose	%%;	bbfont semicolon

  18. infix_properties::=following
    1. binding_power::Nat.
    2. associativity::{left,right}.

    End.
  19. Infix::infix_operator->infix_properties.
  20. Infix::= and+>(7, left) | or+>(6, left) | implies+>(5, right) | iff+>(4, left) | hide+>(3, left) | rename+>(2, left) | schema_compose+>(1, left).
  21. Schema_Text::= Declaration O(bar Predicate).

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

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

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

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

  27. Rel::= "=" | \in | Infix_Rel.

  28. Expression_0::= \lambda Schema_Text big_dot Expression | \mu Schema_Text O(big_dot Expression) | Expression.

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

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

  31. Expression2::= Expression_2 Expression_3 | Expression_3.

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

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

  34. Ident::= Word Decoration.

  35. Decl_Name::= Ident | Op_name.
  36. Var_Name::= Ident | left_paren Op_Name right_paren.

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

  38. Infix_Sym::= Infix_Fun | Infix_Gen | Infix_Rel.
  39. Prefix_Sym::= Prefix_Gen | Prefix_Rel.

  40. Gen_Formals::= "[" List(Ident) "]".
  41. Gen_Actuals::= "[" List(Expression) "]".

  42. Word::@lexeme=undecorated name of special symbol.
  43. Stroke::@lexeme= "'" | "?" | "!" | subscript_digit.
  44. Decoration::@lexemes=It may be the same as a Stroke?, -- see [ roadworks.html ]

  45. Infix_Fun::@lexeme=Infix function symbol.
  46. Infix_Rel::@lexeme=Infix relation symbol.
  47. Infix_Gen::@lexeme=Infix generic symbol.
  48. Prefix_Gen::@lexeme=prefix generic symbol.
  49. Prefix_Rel::@lexeme=prefix relation symbol.
  50. Postfix_Fun::@lexeme=postfix function symbol.
  51. Number::=unsigned decimal integer.

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

Formulae and Definitions in Alphabetical Order