TLZ (Abstract)

Z is a formal specification language that describes a system by writing actions–essentially the same kinds of actions that appear in a TLA specification. It was developed by Mike Spivey and others at Oxford for specifying sequential programs. When someone develops a method for sequential programs, they usually think that it will also handle concurrent programs–perhaps by adding an extra feature or two. I had heard that this wasn’t true of the Z developers, and that they were smart enough to realize that Z did not handle concurrency. Moreover, Z is based on mathematics not programming languages, so it is a fairly nice language.

TLA assumes an underlying logic for writing actions. The next step was obvious: devise a language for specifying concurrent systems that extends Z with the operators of TLA. Equally obvious was the name of such a language: TLZ.

In the Spring of 1991, I visited Oxford and gave a talk on TLA, pointing out how naturally it could be combined with Z. The idea was as popular as bacon and eggs at Yeshiva University. Tony Hoare was at Oxford, and concurrency at Oxford meant CSP. The Z community was interested only in combining Z with CSP–which is about as natural as combining predicate logic with C++.

A couple of years later, I was invited to give a talk at the Z User’s Meeting. I dusted off the TLZ idea and presented it at the meeting. Again, I encountered a resounding lack of interest.

Had TLA been adopted by the Z community, it might have become a lot more popular. On the other hand, not being attached to Z meant that I didn’t have to live with Z’s drawbacks and was free to design a more elegant language for specifying actions. The result was TLA+, described in [127].