| The Z notation is a symbolic language for formal specification of
algorithms. The reference manual for Z is "The Z Notation, A Reference
Manual" by J.M. Spivey, Prentice-Hall � 1989, ISBN 0-13-983768-X.
From chapter one:
"1.1 What is a formal specification?
Formal specifications use mathematical notation to describe in a
precise way the properties which an information system must have,
without unduly constraining the way in which these properties are
achieved. They describe *what* the system must do without saying *how*
it is to be done. This *abstraction* makes formal specifications
useful in the process of developing a computer system, because they
allow questions about what the system does to be answered confidently,
without the need to desentagle the information from a mass of detailed
program code, or to speculate about the meaning of phrases in an
imprecisely-worded prose description..."
Z is based on set theory, predicate calculus, temporal logic, and
function mapping. The Software Engineering Institute (SEI) Pittsburg,
PA has a book by Woodcock called "Software Engineering Mathematics"
that uses Z. SEI is using Z as its formal specification notation. The
main usefullness of Z (as I see it) is its schema technique that allows
modularization of formal specifications that allows composition of
systems from formally specified primatives that allows complex
reasoning about systems without having to reason from first principles.
Hence it is the symbolic mathematical manipulation that should be of
interest to the participants of this notes conference.
|
| ref .-1
Yes, this too is true. I've read through the book by Cliff Jones
"Systematic software development using VDM" and while I find VDM an
interesting notation I find that it suffers from the concept that
proofs are monolithic. Z has the features that schemas (modules) can
re-use other schemas as well as the concept of generic (chapter 2.4 in
book ref. .0) schemas. I also see Z as a regular and orthoginal
notation hence lending itself to compilation and automated proofs; not
to say that VDM does not, though I find too many intuitive steps in
VDM to allow general proofs to be automatically manipulated.
In reference to the topic, I'd like to post Z schemas and start a
discourse. I'm hoping to find Z "speakers" out here in notes-land.
I'll have to resort to ASCII "munges" for the notation though. For
example the existential qualifier would be "|E" for backwards "E" and
the universal qalifier would be "|A" for upside-down "A", et.al., etc.
Anybody out there?
Richard
|