Background (On The Semantics of Z)

At the beginning of 1990 ICL began a collaborative R&D project called the FST project. An important objective of this project was to implement best achievable proof support for the Z specification language.

The intended approach to providing proof support was using a "semantic embedding" of Z into HOL, using a new implementation of HOL to be undertaken under the project. While the first prototype of what was then known as "ICL HOL" was being implemented I considered how much of Z might be approached in this way, and how closely we could approach the semantics as it was then known.

I had already expressed reservations about the treatment of undefinedness published the previous year in Understanding Z. On this point it seemed to me better to argue in favour of a more classical treatment of undefinedness. The alternative was to put considerable effort into realising an approach which seemed to offer no real benefit but gave less convenient proof rules.

After some deliberation I came up with an approach to the embedding which would cover the entire language, which which would get the semantics, on all points other than undefinedness, on the nail. A key difficulty was in realising all of the elaborate variable binding constructs, and in replicating the strange rules about occurrences of variables in Z (not all of which are visible), in a semantically accurate mapping into a much better behaved language with just one variable binding construct. Another problem was the treatment of the unique set parameterised generic constructs found in Z.

At this time the British Government was funding the development of a (different) Z tool by a consortium including SD-Psicon(?) (now EDS) and Imperial Software Technology (IST), and held regular seminars attended by representatives from ICL, IST, other HMG contractors involved in formal methods, and also some academics, including Jim Woodcock. These seminars were a good place to discuss the semantics of Z and its relation to proof theory, and I gave a series of talks in this context explaining our approach and comparing it with alternatives.

None of this material has ever been published, (or even written up) though some of the overheads have been made available to enquiring individuals (provoked by a reference in the first paper published by Woodcock and Brien on their logic for Z).

Z UP HOME © Roger Bishop Jones created 22/6/95 modified 22/6/95