home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1993 #3 / NN_1993_3.iso / spool / comp / specific / z / 540 < prev    next >
Encoding:
Text File  |  1993-01-27  |  1.5 KB  |  38 lines
  1. Newsgroups: comp.specification.z
  2. Path: sparky!uunet!digex.com!intercon!udel!gatech!ncar!destroyer!cs.ubc.ca!uw-beaver!jon
  3. From: jon@cs.washington.edu (Jon Jacky)
  4. Subject: Re: Z and other design methodologies
  5. Message-ID: <1993Jan27.174047.20467@beaver.cs.washington.edu>
  6. Summary: Z can easily model state transition diagrams
  7. Keywords: Z, state transitition diagrams
  8. Sender: news@beaver.cs.washington.edu (USENET News System)
  9. Organization: Computer Science & Engineering, U. of Washington, Seattle
  10. References: <1993Jan26.154610.27454@spectrum.xerox.com>
  11. Date: Wed, 27 Jan 93 17:40:47 GMT
  12. Lines: 24
  13.  
  14. In article <1993Jan26.154610.27454@spectrum.xerox.com> kirby@xerox.com writes:
  15.  
  16. > One of the most useful features of your 
  17. > traditional design and analysis methodologies (like rumbaugh, shlaer/mellor,
  18. > etc..) is the state-transition diagram.  Is there a way in Z to model not 
  19. > only  the states, but the transitions into and out of different states? 
  20.  
  21. Yes.  If S is the state schema that contains the state variables 
  22. for the subsystem modelled by the diagram,
  23. then each bubble in the diagram represents a set of states distinguished
  24. by some predicate on those variables.   So, bubbles labelled A and B can be 
  25. represented by Z state schemas also:
  26.  
  27.     SA =^=  [ S  | ... predicate for state SA ... ]
  28.  
  29.     SB =^=  [ S  | ... predicate for state SB ... ]
  30.  
  31. Then the transition from A to B is simply:
  32.  
  33.     TrAB =^=  SA /\ SB'
  34.  
  35. - Jon Jacky, jon@radonc.washington.edu, University of Washington, Seattle USA
  36.  
  37.  
  38.