Syntax of The Formal Specification Language Z

MATHS

math.syntax.html

When used for syntax it close enough to EBNF to be called XBNF. The following special forms are used in syntax

L(X,Y)::=X #(Y X), list of X's separated by Ys.
List(X)::=X #("," X), list of X's separated by Ys.
#X::=any number of X including none.
O(X)::= (|X), optional X.
definer::= ":" ":" "=", two colons and an equalsign.
EOLN::=end of line.
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. For more on Τ_ΕΧ and ASCII see: [ comp.text.TeX.html ] [ comp.text.ASCII.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.
There is an excellent simple text that shows how to use Z to specify digital systems:
- [Wordsworth93] and a short put accurate Wikipedia entry: [ Z_notation ]
  
  Grammar
  The following is based on [Spivey89]
- Specification::= L(Paragraph, EOLN).
- Paragraph::= Declare_generic_sets| Box | Schema_Name O( Gen_Formals) Define_symbol Schema_exp | Def_Lhs "==" Expression | Ident definer L(Branch, "|") | Predicate.
- Declare_generic_sets::= "[" List(Ident) "]" .
- Box::= Axiomatic_Box | Schema_Box | Generic_Box.
- Define_symbol::=equals sign with circumflex accent.
- Axiomatic_box::= start_axiom Decl_part Possible_Axioms end_axiom.
- Possible_Axioms::=O( EOLN such_that EOLN Axiom_part).
  Email Form
```
  	+..
```
```
  	  Decls
```
```
  	|--
```
```
  	  Axioms
```
```
  	-..
```
  It looks like this:
```
 	| Decls
```
```
 	|-------
```
```
 	| Axioms
```
- 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
```
```
 	 ----------------------
```
- 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
```
```
 	 ------------
```
- 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 ")"
- and::lexeme, infix_operator.
- or::lexeme, infix_operator.
- implies::lexeme, infix_operator.
- iff::lexeme, infix_operator.
- hide::lexeme, infix_operator.
- rename::lexeme, infix_operator.
- compose::lexeme, infix_operator.
- infix_operator::= Infix.EMail. I've chosen, below, to model infix operators as a table of properties with the lexemes in the EMail notation:
- Infix::@infix_properties=following,
  Table
  Name Binding power associativity EMail TeX MATHS
  and 7 left /\ ∧ and
  or 6 left \/ ∨ or
  implies 5 right ==> \implies if_then_
  iff 4 left <=> \iff iff
  hide 3 left | \vbar some
  rename 2 left \ ? =>
  compose 1 left %%; \bbfont ; ;
  
  (Close Table)
- infix_properties::=following
  Net
  1. binding_power::Nat.
  2. associativity::{left,right}.
  3. EMail::#ASCII.
  4. TeX::#ASCII.
  5. MATHS::#ASCII
  (End of Net)
- Schema_Text::= Declaration O(bar Predicate).
- Schema_ref::= Schema_Name Decoration O(Gen_Actuals).
- Declaration::= L(Basic_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::= "=" | ∈ | Infix_Rel.
- Expression_0::= λ Schema_Text big_dot Expression | μ 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(List(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.
- 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.
- Decoration::@lexeme=Stroke.
- 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.

Name	Binding power	associativity	EMail	TeX	MATHS
and	7	left	/\	∧	and
or	6	left	\/	∨	or
implies	5	right	==>	\implies	if_then_
iff	4	left	<=>	\iff	iff
hide	3	left	\|	\vbar	some
rename	2	left	\	?	=>
compose	1	left	%%;	\bbfont ;	;

. . . . . . . . . ( end of section Syntax of The Formal Specification Language Z) <<Contents | End>>

Contents

Syntax of The Formal Specification Language Z

MATHS

Lexicon

Grammar

End