[ISO] | [JTC1] | [SC22]


WG 19 (Formal Specification Languages) Home Page


What is WG 19?

Welcome to the home page of WG 19, a working group of SC 22, subcommittee of JTC 1, a joint technical committee of ISO/IEC.

WG 19 is responsible for international standards activity on formal methods, formal specification languages, and syntactic metalanguages. It has the following projects under way.

The Convener of WG 19 is Roger Scowen, 9 Birchwood Grove, Hampton, Middlesex TW12 3DU, UK.

Enquiries about the work of the group should be addressed to the Convener.

Back to the table of contents.

Extended BNF

Extended BNF is a syntactic metalanguage based on the BNF notation used in the definition of Algol 60. It is intended for use in all international standards that define languages.

An international standard ISO/IEC 14977 : 1996 Syntactic Metalanguage - Extended BNF has been published and a revision is in progress.

Back to the table of contents.

Formal Specification languages

A formal specification language is a mathematical notation used in software development to express the functional specification of a system. The specification defines what function is provided without saying how it will be provided.

There are many such notations used in software development, but only two of them have been the subjects of international standardization:

Back to the table of contents.

The VDM project

The Vienna Development Method is a complete software development method. Its specification language is VDM-SL. The following notes about VDM are based on the Introduction to the international standard for VDM-SL, ISO/IEC 13817-1: 1996.

The Vienna Development Method originated in work done in IBM's laboratory in Vienna in the 1970s. The first complete exposition of the notation and method was Jones's book Software Development: A Rigorous Approach.

A standard for the base language of VDM-SL was published in 1996.

Back to the table of contents.

The Z Notation project

The Z notation is a specification language based on set theory and predicate calculus. It arose from work of Jean-Raymond Abrial in the late 1970s, and was taken up and expanded by the Programming Research Group of the Oxford University Computing Laboratory. Z was used in the 1980s in a number of industrial projects to assist developers of hardware and software systems. The notation was defined formally by Spivey in his book Understanding Z (1988), and this was followed by an informal description and guide to the notation in The Z Notation: A Reference Manual (1989, 2nd edn 1992). Industrial users of Z pressed the PRG, guardians of the notation, to produce a definitive statement about the content of the Z language, and this resulted in a collaboration of academic and industrial users in the ZIP project. ZIP was a five-year project funded partly by the UK government, and partly by the collaborators. It included other things as well as language definition. When ZIP ended, the language definition committee continued its work by developing an international standard within WG19.

A Final Committee Draft, ISO/IEC FCD 13568, was approved in March 2001, and an FDIS (Final Draft International Standard) has been sent for balloting. It is expected that the standard will be published in 2002.

There is more information on Z at The Z Notation.

Back to the table of contents.


Back to the table of contents.

Created 1998 by J. B. Wordsworth; updated in 2001 by R. S. Scowen.