🚀 go-pugleaf

RetroBBS NetNews Server

Inspired by RockSolid Light RIP Retro Guy

Thread View: comp.specification.z
3 messages
3 total messages Started by Frazer Middleton Tue, 05 Jan 1993 16:28
Z Animation in Prolog
#135
Author: Frazer Middleton
Date: Tue, 05 Jan 1993 16:28
99 lines
3981 bytes
Firstly, may I introduce myself to the Z forum....
My name is Frazer Middleton and I am working for IBM UK Research Laboratories,
Hursley Park, Hampshire. As you probably know by now, we are redesigning our
main product (CICS) using Z. However, I am not involved with this area, but I
have a personal interest in Z and use it for my own code. I am also interested
in the animation of Z specs in Prolog. Late last year, I asked one of my
colleagues (Mr John Wordsworth) if he had any information on animating Z specs
using Prolog, and he placed an append on the forum on my behalf, and received
references from many people about the subject, some of whom asked for a precis
to be appended to the net..... here it is!

My thanks go to all who supplied any information on the subject.....

Title  : Software Development: Two approaches to animation of Z specifications
         using Prolog
Authors: Margaret M West, Barry M Eaglestone
Journal: Software Engineering Journal
Pages  : 264 - 276
Date   : July 1992


Title  : The Implementation of Z Specifications using Program Transformation
         Systems: The SuZan Project
Authors: C Rattray, R G Clark (Editors)
Journal: "The Unified Computation Laboratory" IMA Conference Series No35
Pubs.  : Clarendon Press, Oxford
Pages  : 207 - 220
Date   : 1992
ISBN   : 0-19-853684-4


Title  : Using Prolog to Animate Mathematics
Authors: D R Brough (Editor)
Journal: Proceeding of the Association for Logic Programming UK-90 Conference            (Logic Programming)
Pubs.  : Intellect Books
Pages  : 173 - 188
Date   : 1992
ISBN   : 0-7923-1546-4


Title  : Making Discrete Maths Executable on a Computer
Authors: ????
Journal: "The Mathematical Revolution Inspired by Computing" IMA Conference
         Series No30
Pubs.  : Clarendon Press, Oxford
Pages  : 127 - 144
Date   : 1991
ISBN   : 0-19-853658-5


Title  : A guide to using the Mathias Prolog library for Discrete Mathematics
         (Second Edition)
Authors: ????
Journal: University of Surrey Computing Science Technical Report CS-92-01
Date   : September 1992


Title  : Declarative Programming for Mathematical Exploration
(Invited presentation at the IMA conference on Artificial Intelligence in
 Mathematics 3-5 April 1991, University of Strathclyde. Proceedings to appear)


Title  : Animating Set-Theoretic Specifications using Prolog (Collected Papers)
Authors: R.D.Knott, P.J.Krause, P.J.Byers
Journal: Technical Report, Department of Mathematical and Computing Science,
         University of Surrey
Date   : 1989


Title  : Alvey Project SE/090:"Implementation of Z specifications using Program
         Transformation systems" locally known as "SuZan" (Surrey University Z
         ANimator) with D H Pitt;
Date   : 10/86 to 12/89


Title  : Formal Specification of an Access Control System
Authors: Susan Stepney, Stephen P Lord
Journal: Software Practice and Experience
Pages  : 575 - 593
Volume : 17
Number : 9
Date   : September 1987


Title  : Z: An introduction to Formal Methods
Authors: Antoni Diller
Pubs.  : John Wiley
Date   : 1990

--------

That just about sums up the list that I have. Mark Hewitt has also done some
interesting work for his BSc and MSc in this area, and he has a couple of
reports on the subject.I can supply his NetID if anyone is interested.
I also have the names of a few people who are also interested in this area, if
you would like their names or NetIDs, then please don't hesitate to contact me
(Fraz@vnet.ibm.com). Many thanks!
                                                                       -Fraz-
PS Happy New Year!
Request: Introductory Z readings, scope of usage
#136
Author: Tom R. Peterson (consultant)
Date: Wed, 06 Jan 1993 17:18
12 lines
823 bytes
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?
2) How long has it taken you to comfortably spec in Z?
3) Does Z include interface design components?
4) What introductory reading is recommended?  Is there a FAQ?

Thank you,

Tom Peterson
trp@gtech.com
Re: Request: Introductory Z readings, scope of usage
#139
Author: Jon Jacky
Date: Thu, 07 Jan 1993 18:43
77 lines
4900 bytes
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
Thread Navigation

This is a paginated view of messages in the thread with full content displayed inline.

Messages are displayed in chronological order, with the original post highlighted in green.

Use pagination controls to navigate through all messages in large threads.

Back to All Threads