(A)nna to (Z)ed
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:

A Condensed Overview of Z

(The Zed Page - Oxford)

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.

Lunch Special Number 1:
General Zed Info

Z Schemas

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

Lunch Special Number 2:
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 ) for further information.

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.

Publications

The following books concerning Z are available:

Other "Formal" Dining Establishments in the Area
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.