**Arila Atanassova-Barnes**(The Inventive One)**Maysa Peterson**(The Creative One)**John Motts**(The Logical One)- Oxford's Z Forum
- Oxford's Z Forum - TeX files
- - I.Hayes (ed.), Specification Case Studies, Prentice Hall International Series in Computer Science, 1987. (2nd ed., 1993)
- - J.M.Spivey, Understanding Z: A specification language and its formal semantics, Cambridge University Press, 1988.
- - D.Ince, An Introduction to Discrete Mathematics, Formal System Specification and Z, Oxford University Press, 1988. (2nd ed., 1993)
- - J.C.P.Woodcock & M.Loomes, Software Engineering Mathematics: Formal Methods Demystified, Pitman, 1998. (Also Addision-Wesley, 1989)
- - J.M.Spivey, The Z Notation: A Reference Manual, Prentice Hall International Series in Computer Science, 1989. (2nd ed., 1992) [Widely used as a de facto standard for Z. Often known as ZRM2.
- - A.Diller, Z: An Introduction to Formal Methods, Wiley, 1990. J.E.Nicholls (ed.), Z user workshop, Oxford 1989, Springer-Verlag, Workshops in Computing, 1990.
- - B.Potter, J.Sinclair & D.Till, An Introduction to Formal Specification and Z, Prentice Hall International Series in Computer Science, 991.D.Lightfoot, Formal Specification using Z, MacMillan, 1991.
- - A.Norcliffe & G.Slater, Mathematics for Software Construction, Ellis Horwood, 1991.
- - J.E.Nicholls (ed.), Z User Workshop, Oxford 1990, Springer-Verlag, Workshops in Computing, 1991.
- - I.Craig, The Formal Specification of Advanced AI Architectures, Ellis Horwood, 1991.
- - M.Imperato, An Introduction to Z, Chartwell-Bratt, 1991.
- - J.B.Wordsworth, Software - Development with Z, Addison-Wesley, 1992. S.Stepney, - R.Barden & D.Cooper (eds.), Object Orientation in Z, Springer-Verlag, Workshops in Computing, August 1992.
- - J.E.Nicholls (ed.), Z User Workshop, York 1991, Springer-Verlag, Workshops in Computing, 1992.
- - D.Edmond, Information Modeling: Specification and Implementation, Prentice Hall, 1992.
- - J.P.Bowen & J.E.Nicholls (eds.), Z User Workshop, London 1992, Springer-Verlag, Workshops in Computing, 1993.
- - S.Stepney, High Integrity Compilation: A case study, Prentice Hall, 1993.
- - M.McMorran & S.Powell, Z Guide for Beginners, Blackwell Scientific, 1993.
- - K.C.Lano & H.Haughton (eds.), Object-Oriented Specification Case Studies, Prentice Hall International Object-Oriented Series, 1993.
- - B.Ratcliff, Introducing Specification Using Z: A practical case study approach, McGraw-Hill, 1994.
- - A.Diller, Z: An Introduction to Formal Methods, 2nd ed., Wiley, 1994. J.P.Bowen &J.A.Hall (eds.), Z User Workshop, Cambridge 1994. Springer-Verlag, Workshops in Computing, 1994.
- - R. Barden, S.Stepney & D.Cooper, Z in Practice, Prentice Hall BCS Practitioner Series, 1994.
- - D.Rann, J.Turner & J.Whitworth, Z: A Beginner's Guide. Chapman & Hall, 1994.
- - D.Heath, D.Allum & L.Dunckley, Introductory Logic and Formal Methods. A.Waller, Henley-on Thames, 1994.
- - L.Bottaci and J.Jones, Formal Specification using Z: A modelling approach. International Thomson Publishing, 1995.
- - D.Sheppard, An Introduction to Formal Specification with Z and VDM.McGraw Hill International Series in Software Engineering, 1995.
- - J.P.Bowen & M.G.Hinchey (eds.), ZUM'95: The Z Formal Specification Notation, Springer-Verlag, Lecture Notes in Computer Science, volume 967, 1995.
- - J.P.Bowen, Formal Specification and Documentation Using Z: A Case Study Approach, International Thomson Publishing, 1996.

- Larch Project at SRC Home Page
- Who's Who on the Web in Formal Methods
- Teesside B-Resource
- The World Wide Web Virtual Library: The Z notation
- The Z formal specification notation
- WWW Virtual Library: Formal Methods - The B-Method
- LaTeX help On-Line Guide
- Formal Methods & their Role in Developing Safe Systems - Workshop report 20.3.95
- Object-Z
- FOOM and Object-Z
- Integrating Object-Oriented Analysis and Formal Specifications
- Formal Specifications in Z
- Centre for Information Systems Research (Formal Methods, Z, and Object-Z)
- Software Engineering Publications
- Software Engineering Sites
- Directory of /pub/anna

Recipes For Formal Specifications

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
systems.

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?"**

**A**ppetizers and Starters | **B**asic
Lunch Items | **C**hef's Special of the Day| **D**essert
and Beverages

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.

General Zed Info

- 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.

**Operations:**

- 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.

Zed Development Tools

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
"zed2e.tex" useful.

** 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
Department.

The following books concerning Z are available:

For your Refined Culinary Pleasure

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

Zed Example

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......

Before your eyes redden, your skin turns green and sheds, your cat runs off screaming, you rip the phone off the wall with your teeth and lay helplessly on the floor drooling all over yourself, ....... Yikes! Go Ahead, sit back and play a game or two before returning to your studies.

tell us what you're
doing with formal specifications

by emailing to: (music"Whoa"man)
maysa@www.kneehighs.com

Zed Soup Supports

Zed Soup is best viewed with Netscape 3.0

LinkExchange Member