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.

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