🚀 go-pugleaf

From article <1992Aug3.222716.21723@beaver.cs.washington.edu>, by jon@cs.washington.edu (Jon Jacky):
> 
> I think they could be complementary and both might be helpful.
> 
> In a state transition diagram, each bubble represents a set of states that 
> satisfy some predicate --- the predicate that expresses what it means for the
> system to be in that state.  So, each bubble could be described by (for
> example) a Z state schema.  Each arrow in the diagram represents a transition
> from a state in one such set to a state in another, so it could be described 
> by a Z operation schema.  
> 
> You can imagine having a specification with a couple of pages of Z schemas,
> then a figure picturing a state transition diagram.   The bubbles and arrows
> in the diagram are each labelled with a name --- the name of one of the
> schemas!   Then you look up that schema to see the full definition of what's
> going on in that bubble (or arrow).   So, the Z serves as annotation for the
> diagram, or the diagram illustrates some of the properties of the Z, depending
> on which way you want to look at it.

I agree with what you have said.

In my Phd thesis I have a Z specification of an event based user
interface that runs to quite a number of pages. Using Z specs
alone would be close to unintelligible, so I started off with
a state transition diagram showing how the different bits fit
together and then wrote the Z specs from it in pretty much the
way described above.

		Lucy Chubb.

Softway Pty Ltd,		Phone: +61 2 698 2322;
P.O. Box 305,			Fax: +61 2 699 9174;
Strawberry Hills,		Email: lucyc@softway.oz.au
NSW 2012,
AUSTRALIA