From: jon@cs.washington.edu (Jon Jacky)
Subject: Re: Request: Introductory Z readings, scope of usage
Summary: Z is a specification notation, not a programming language
Keywords: Z, C, formal specifications
Organization: Computer Science & Engineering, U. of Washington, Seattle
Date: Thu, 7 Jan 93 18:43:54 GMT

In article <1993Jan6.171823.23872@gtech.com> trp@gtech.com (Tom R. Peterson (consultant)) writes:
> Other than scanning software eng. materials in bookstores, I
> have not been exposed to Z, and have a couple questions:
>
> 1) Would Z have any advantage over C for 2-3 person teams?

Well, C is an executable programming language, but Z is a non-executable 
notation (as is English, and much of math) for writing specifications.  So, 
if you write your C programs to meet some requirements that can be expressed 
in advance, Z might be useful; it is certainly much more expressive and clearer
than C for describing many things.  

Don't think of Z as if it were a programming language!  It plays a different
role entirely.

Also, team size doesn't have much to do with how useful it is.  In some 
applications it is important for even one person to write down the 
requirements before plunging into coding.  With something as little-known 
as Z is now, small size may be an advantage: even if you are the only one in 
your organization who knows Z, 50% of your two-person team will be familiar 
with the notation!

>2) How long has it taken you to comfortably spec in Z?

I've been experimenting with Z for over three years.  The specs I've written
in the last ten months or so haven't been half bad.  Before that, most of them
were awful, I now realize.   

The right question to ask isn't "how comfortable is it to write specs," but 
"how comfortable is it to *read* them"!   Good specs are hard to write but easy
to read, bad specs are easy to write but just about impossible to understand.
So, you can learn to read and understand Z quickly, but writing it well takes
much longer.

I think most people have found that it is quite difficult to write 
Z expressively and well, in applications other than the small databases that 
tend to dominate the tutorial materials.  Partly this is just the inherent
difficulty of expressing exactly what you want, no more and no less, instead
of just plunging on and building something that does sort of what you had in 
mind, more or less.  Partly it's because years of programming tends to warp
your mind in a particular direction that makes it especially difficult to
grasp what should be going on in notations such as Z.

>3) Does Z include interface design components?

Z hardly includes anything!  It includes sets, tuples, relations, functions,
sequences and bags, ordinary first-order logic, and a few ways to structure 
the specification text, most
notably the "schema", which is almost the only construct that distinguishes
Z from bare discrete math.   You can use schemas to model record-like data
structures, among other things.  Oh, and it has numbers and arithmetic, too.

In Z it's up to you to model your system out of these elements. 

>4) What introductory reading is recommended?  Is there a FAQ?

There is a FAQ with a list of every Z book ever published.  Watch this space.

The first
chapter of Spivey's Z Reference Manual (Prentice-Hall International "red book"
series) is probably the best place to start.   Woodcock and Loomes' "Software
Engineering Mathematics" (Addison Wesley), while not just a Z book, is a very
good introduction to the approach used in Z and uses a notation that is close 
enough to Z for almost anyone.  Also, you can actually find this book in the 
USA. There are now at least four textbooks that are fairly comprehensive 
introductions to Z and the discrete math in Z: Potter, Sinclair and Till,
"An Introduction to Formal Specification and Z" (another Prentice-Hall red 
book), Diller, "Z: An Introduction to Formal Methods" (Wiley UK), Wordsworth, 
"Software Develoment with Z" (Addison Wesley UK) and Ince, "An Introduction to
Discrete Math and Formal System Specification" (Oxford U Press).  These will 
all put you on the right track.  There are others in the FAQ as well, 
that I haven't seen.  Hayes' "Specification Case Studies" is the original
classic, has bigger and more realistic examples that the textbooks, yet 
another Prentice Hall red book, hasn't been seen in US bookstores
in ages, try interlibrary loan.

- Jon Jacky, jon@radonc.washington.edu, Univ. of Washington, Seattle