(c) University of Southampton 1994
Contents
Not all mathematics is easy to read. Sometimes the author has chosen an unfortunate form of expression. Sometimes there was no better notation available. This article contains a list of possible extensions to the Z notation that other authors may wish to adopt for use in their specifications. Each extension abbreviates a commonly occuring construct in Z. In most cases the proposed abbreviation is in common use in some other branch of mathematics or computing.
There is much to be said against extensions to the Z notation. Mike Spivey in his reference manual [5] quotes from Katherine Whitehorn's Cooking in a Bedsitter ``the right simple tools will stop you longing for the other, complicated ones''. And indeed, in the second edition he has added only 13 or so new symbols. Another reason for avoiding extensions is the wish to remain within a standard set of notations. This is relevant as work on the Z standard continues [1].
Nonetheless it is wise to be aware of the limitations of any tool. Exploring possible extensions to a notation is one way to expose its limitations.
When students are asked to write their first Z specification, they often produce formulae that are not Z. Some of these formulae have no obvious meaning; others make sense, but happen not to conform to Z syntax and semantics. These latter examples have inspired many of the suggestions that follow. A particular point to note is the influence of the functional programming language Standard ML [3] which we teach at Southampton as the first programming language [2]. Students naturally borrow concepts and notations from SML, which is a declarative language, and attempt to use them in Z. Unfortunately, the correct Z equivalent can be verbose and clumsy in comparison, particularly when defining a function.
This rather undermines the slogan I like to use in advertising Z, namely that it is a notation both precise and concise. Of all the abbreviations below, I believe that the most important are those that facilitate the definition of functions.
Where possible I illustrate each proposed extension with an example from Spivey's Z reference manual (which I will refer to from now on as the ZRM) showing how it could be improved by the new notation.
Authors should have the freedom to write this, if they so choose, as
Purists who find this too operational may prefer the equivalent formulation
Including both conditional expressions and predicates would be less confusing to authors familiar with functional programming (in which predicates are just one type of expression). The quantifier let can be applied to both expressions and predicates. The same should be true also of if then else.
In standard Z these definitions must be augmented with declarations
In its favour the mathematical style is shorter, and is widely
known. In the two examples given, the types of IMG ALIGN=BOTTOM
SRC="_13049_tex2html_wrap215.gif"> and 
can
be inferred from the given predicates. The traditional style of
set comprehension is syntactically distinct from the standard Z
style, as only Z style comprehensions have declarations. It is
therefore possible to add traditional set comprehensions to
Z without introducing ambiguity.
To be specific, the set comprehension 
-
should be allowed as an abbreviation for
where 
is the free variable (or variables) of 
and
is its type (or types). This form is allowed only where the
type (or types) can be inferred. The standard Z form can be used where
type inference would fail, or else where it is desired to emphasise
the types involved.
Other constructs in Z already admit similar abbreviations, for example the lambda expression.
Suppose a printer queue is modelled as a sequence of pairs, user and data to be printed.
Consider an operation that displays in order the user and size of each data file in the queue over 100KBytes in size. The key equation is
Using sequence comprehension this could be written without introducing
the distracting index 
. This leads to schemas such as
I would like to propose the notation 
to help in
abbreviating this. The operation 
would then be written
A formal definition of this notation would use schema tuples and the theta notation.
This, which is nearly correct Z, states that the state vector 
excluding variables in the given list is equal to the state vector
with corresponding variables also excluded.
convention as
follows: 
is short for the conjunction over all variables
in 
of the equations
.
With this convention, the schema could be written
is a schema,
is the same schema, but with substituted for
. A
restriction is that must be a variable; it cannot be an expression.
It is useful to extend renaming so that expressions can be used. For
example, 
would
constrain 
in the same
way that
constrains . The
notation 
where is a schema, 
an
expression, and a variable is an abbreviation for
where 
is a fresh variable.
My concern here is with the constraint governing the number
of the first line in the window, 
. The predicate 
ensures that the window is moved if need be so
that the line containing the cursor is present in the 25 line window.
(Presumably other predicates describe any horizontal scrolling that
may be required - for simplicity these have been omitted.)
Unfortunately, this predicate alone is too weak. There are 25
possible values for 
that satisfy it. Another rule is
required to restrict the non-determinism. For example we might
to require that the window should move only as far as needed to
ensure that it contains the cursor. The 
operator, which
combines a schema and an expression to form a new schema, allows a
convenient formalisation of this rule.
This abbreviates the schema
The only difficulty in the definition of the operator
is in knowing which variables to quantify over. My suggestion is
any primed or output variables that occur free in the expression to
be minimised. In the example above, the only such variable is the
primed variable .
The dual 
operator can easily be defined
flat, also
called distributed concatenation. Paulson [4] gives
fun flat [] = []
| flat(l :: ls) = l @ flat ls
Here [] is the empty list, :: denotes list construction, and
is used to append (or concatenate) two lists.
We see in this one definition all three significant features of a modern functional programming language: definition by cases (using patterns), recursion, and type inference. These three features are supported, but only weakly, in the current Z standard. As a result, the Z definition of distributed concatenation is relatively clumsy and confusing.
Just as a free type definition is an allowable abbreviation for an axiomatic declaration, so too the following function definition should be allowed.
This definition, which closely mimics the SML definition given above, is an abbreviation for the least fixed point defined, in standard Z, as
