WELCOME to Zed Soup! We're a friendly bunch, with a corner cafe motif, nestled between the Endless Mountains and the Pocono Mountains (Honeymooner's Heaven). We, The Formal Specifications Team, developed this site at the University of Scranton, Software Engineering Department, under the direction of John Beidler, Ph.D.
In studying the necessity for providing formalized methods
to software specifications, analysis and design, it became apparent that
there exists a spectrum of possible approaches for software engineers to
take. Some tools, available in this area, provide annotated programming
languages that support assertion testing alongside syntactic compilation.
Others were separate executables that were developed simultaneously with
analysis/design in order to track, report, and correlate assertions (pre-
and post-conditions) to provided code. This is achieved through pre-processed
"assertive" executables. In some cases, the tools provided for
formal specifications were simple assertion text-editing applications.
Some in the field are working on formally proving assertions using mathematical
methods, guarded command language (dysktra), or mathematical notation -
as is Z(ed).
In Australia, Paul Swatman's team is working on a methodology
and tools that combine Object-Z, Object-Oriented Analysis and Design, along
with textual supplimentation, Class and Object Diagrams to fully and consistently
specify software systems. Having identified that the majority of system
errors are introduced in the analysis and early design stages, it is obvious
that there exists a necessity to stabilize software development in this
area if we wish to provide reliable, reusable, and retainable software
Our Formal Specifications Team have chosen to focus our studies on Z and the feasibility of applying it to the generation of large and complex software projects in industry today. But first, let us introduce ourselves.
The Formal Specifications Team Members include:
"May I take your order please?"
Z is a formal specification notation based on set theory and first order
predicate logic. It has been developed at the Programming Research Group
at the Oxford University Computing Laboratory (OUCL) and elsewhere since
the late 1970s.
Z is a (non-executable in general) specification language, no Z compiler/linker/etc. is needed as in programming languages. Some people have looked at animating subsets of Z for rapid prototyping purposes, using logic and functional programming for example, but this work is preliminary and is not really the major point of Z, which is to increase human understandability of the specified system and allow the possibility of formal reasoning and development.
The Programming Research Group is especially known for its pioneering research on programming language semantics, including Scott-Strachey denotational semantics, for its development of the CSP approach to concurrent processes, and for the Z specification language. More recent research has developed the occam language, methods to ensure the correct production of software and hardware, the functional programming language Orwell, and the 2OBJ and Jape logical frameworks for theorem proving, hardware compilers and optimizers, and game-theoretic models of higher-order programming.
Many of its research projects consist of mathematical theories with
their experimental validation and evaluation.
The comp.specification.z USENET newsgroup provides a forum for messages
concerned with recent developments and the use of Z. Pointers to and reviews
of recent books and articles are particularly encouraged.
- A specification in Z is a collection of schemas.
- A schema contains specification entities and the relationships between these entities.
- Parts of a schema include:
- 1. The top line of the schema contains the schema name.
- 2. Below the top line and above the dividing line is the signature where the names and types of the entities are introduced.
- 3. The predicate (bottom part) sets out the relationships between the entities in the signature by defining a predicate over the entities which must always hold.
- The effect of combining specifications is to make a new specification which inherits the signatures and predicates of the included specifications.
- Inherited signatures and predicates are combined with any new signatures and predicates which are introduced in the new specification.
- The predicates are written on separate lines and an implicit and separates them.
- Names whose final character is a ? are always taken to indicate operation inputs.
- Names whose final character is a ! are always taken to indicate operation outputs.
- The values of an entity after an operation are referenced by adding the suffix quote mark (') to the entity name.
- The delta schema (represented here by the ^ symbol) indicates that the effect of the operation is likely to change one or more values of the schema's entities.
Specification Using Functions
- Functions can be used to model data structures.
- A schema can define a partial function by use of the tagged arrow indicator. Then, given a name, the associated type and description can be discovered.
- The enclosure of the schema name in curly brackets defines a set. The name of the set is in upper-case characters.
- The name of a partial function is used in the same way as a function name in a programming language, with the name acting as a parameter.
- A function is an abstraction over an expression in programming languages.
- In Z, a function is a set of pairs where each pair shows how an output relates to an input.
- A partial function is a function where not all possible inputs have a defined output.
- The domain of a function is the set of inputs over which the function has a defined result.
- The range of a function is the set of results which the function can produce.
- If an input is in the domain of some function f(i in dom f), the associated result may be specified as f(i), i.e. f(i) in rng f.
Specification Using Sequences
- A sequence is a collection where the elements are referenced by their position in the collection.
- Formally, a sequence of X is a mapping where the positive integers have associated values in X and the domain of the mapping includes all integers from 1 to n where n is the length of the sequence.
Various tools for formatting, type-checking and aiding proofs in Z are available. A free LaTeX style file and documentation can be obtained from the OUCL archive. Access the:
A newer style "csp_zed.sty" is available in the same location,
which uses the new font selection scheme and covers CSP and Z symbols.
A style for Object-Z "oz.sty" with a guide "oz.tex"
is also accessible. LaTeX2e users may find "zed-csp.sty" and
The fuzz package, is a syntax and type-checker with a
LaTeX style option and fonts. It is available from the Spivey Partnership
and is compatible with the 2nd edition of the Z Reference Manual. Access:this
file for brief information and an order form.
OR Contact Mike Spivey (email
CADiZ is a suite of integrated tools for preparing and
type-checking specifications as professional quality typeset documents.
The Z dialect it recognizes has evolved in line with the standard. The
typesetting can be performed by either troff or LaTeX for Unix or Word
for Windows. The mouse can be used to see the expansion of schema calculus
expressions, and to reason about conjectures such as proof obligations.
The PC version is integrated with MS Word using OLE2, providing WYSIWYG
editing of Z paragraphs directly in Word documents. (The troff and LaTeX
versions use ordinary text editors on ASCII mark-up.)
ProofPower is a suite of tools supporting specification
and proof in Higher Order Logic (HOL). Information about ProofPower can
be obtained automatically by sending email to
Zola is a commercial integrated support tool for Z on
Sun workstations, for automated assistance at all stages of the specification
construction, proving and maintenance process. It is intended for system
developers and includes a WYSIWYG editor, type-checker and tactical theorem
prover suitable for the creation and maintenance of large specifications.
ZTC is a Z type-checker available free of charge for educational
and non-profit uses. It is intended to be compliant with the 2nd edition
of Spivey's Z Reference Manual. It accepts LaTeX with "zed" or
"oz" styles, and ZSL - an ASCII version of Z. ZANS is a Z animator.
It is a research prototype that is still very crude. Both ZTC and ZANS
run on Linux, SunOS 4.x, Solaris 2.x, HP-UX 9.0, DOS, and extended DOS.
They are available here in the
directories ZANS-x.xx and ZTC-x.xx, where x.xx are version numbers.
Formalizer is a syntax-directed WYSIWYG Z editor and interactive
type checker, running under Microsoft Windows, available from Logica.
DST-fuzz is a set of tools based on the fuzz package by
Mike Spivey, supplying a Motif based user interface for LaTeX based pretty
printing, syntax and type-checking. A CASE tool interface allows basic
functionality for combined application of Z together with structured specifications.
The B-Tool can be used to check proofs concerning parts
of Z specifications.
The B-Toolkit is a set of integrated tools which fully supports
the B-Method for formal software development and is available from B-Core
(UK) Limited. Z fonts for MS Windows and Macintosh are available on-line.
For hyperlinks to these and other Z tool resources see The
WWW Z Page: . A survey of Z tools may be obtained from Systems Process
The following books concerning Z are available:
Here are some links to other web sites with information on Z and Formal Methods/Specifications for Software:
We're serving up a delicious example of a Z specification for dessert.
We must give credit to the chef who created the schemas...
This example is taken from the book titled, "Z in practice" by Rosalin Barden, Susan Stepney and David Cooper (pages 134 to 142).
The Tower of Hanoi
HERE we have the Zed Specifications for the algorithm of the Tower of Hanoi, along with some textual explanation and animations.
And....HERE is an example of the code written in ADA.
Hope you've found this page useful and interesting. If you find any
other interesting links on formal methods, drop us a line. And now for
something completely different......
tell us what you're doing with formal specifications
by emailing to: (music"Whoa"man) email@example.com
Zed Soup Supports
Zed Soup is best viewed with Netscape 3.0