.Open Syntax of The Formal Specification Language Z
. MATHS
This document is prepared using the MATHS notation
.See http://www/dick/samples/math.syntax.html
and 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.

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.
.See http://www/dick/samples/comp.text.TeX.html
.See http://www/dick/samples/comp.text.ASCII.html

*New* Proposed standard lexemes for ASCII/EMail:
.See http://www/dick/samples/z.lexis.html

There is a computerized code developed at York University England and tools
that translate that into TeX.   
. Grammar
The following is based on
.See [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
.As_is  	+..
.As_is  	  Decls
.As_is  	|--
.As_is  	  Axioms
.As_is  	-..
It looks like this:
.As_is 	| Decls
.As_is 	|-------
.As_is 	| Axioms

Schema_Box::= $start_schema $Schema_Name $O($Gen_Formals) $dash $EOLN $Decl_Part $Possible_Axioms $end.
Email Form
.As_is  	+-- Name ---
.As_is  	  Decls
.As_is  	---
.As_is giving
.As_is 	 -------Name----------
.As_is 	| Decls
.As_is 	 --------------
or
.As_is  	+-- Name ---
.As_is  	  Decls
.As_is  	|--
.As_is  	  Axioms
.As_is  	---
giving this kind of thing:
.As_is 	 -------Name----------
.As_is 	| Decls
.As_is 	|--------------
.As_is 	| Axioms
.As_is 	 ----------------------

Generic_Box::= $start_generic $O($Gen_Formals) $double_dash $EOLN $vertical_bar $Decl_Part $Possible_Axioms.

Email:
.As_is  	+== [Para] ===
.As_is  	  Decls
.As_is  	|--
.As_is  	  Axioms
.As_is  	-==


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

I've chosen to model infix operators as a map that associates the
syntax with its priority and associativity:
infix_properties::=following
.Net
binding_power::Nat.
associativity::{left,right}.
.Close.Net
Infix::infix_operator->$infix_properties,
Infix= $and+>(7, left) | $or+>(6, left) | $implies+>(5, right) | $iff+>(4, left) | $hide+>(3, left) | $rename+>(2, left) | $schema_compose+>(1, left).

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::= "=" | \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($List(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.
Decoration::@lexemes=`It may be the same as a Stroke?`,
.Hole

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 Syntax of The Formal Specification Language Z