Syntax of The Formal Specification Language Z
- 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. [ 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.
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 ")"
- infix_operator::= and| or| implies| iff| hide| rename| schema_compose.
Name EMail TeX MATHS and /\ ∧ and or \/ ∨ or implies ==> \implies if_then_ iff <=> \iff iff hide | \vbar some rename \ ? compose %%; bbfont semicolon semicolon 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}.
(End of 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::= "=" | ∈ | 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::@lexemes=It may be the same as a Stroke?,
[click here
![[socket symbol]](hole.gif)
if you can fill this 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.
MATHS
This document is prepared using the MATHS notation [ 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
. . . . . . . . . ( end of section Syntax of The Formal Specification Language Z) <<Contents | End>>