🚀 go-pugleaf

In article <...> brendan@cs.uq.oz.au (Brendan Mahony) writes:

   I feel that in claiming that timing information is easily included in
   CSP that Jim is modestly undervaluing the years of endeavour that he and
   others have invested in achieving this goal. Those wishing to follow in
   these illustrious footsteps might find a firm grounding in metric space
   topology an asset. 

Thanks for the appreciation.  However, the weirdo mathematics is only needed
to set up the models... in APPLICATIONS of CSP, all you need is a little set
theory... as you've pointed out

   Using CSP within Z required little more than the definition of a new
   data type and some useful operations. Eg CSP trace theory:

   \begin{zed}
   [EVENTS]
   \end{zed}

   \begin{axdef}
   TRCSP : power (\power (\seq EVENTS))
   \where
   \forall P : \power (\seq EVENTS) \spot \\
   \t1	P \in TRCSP \iff \\
   \t1	\lang \rang \in P \\
   \t1	\forall s : \seq EVENTS,; a : EVENTS \spot \\
   \t2		s \cat \lang a \rang \in P \implies s \in P

	   etc
   \end{axdef}

   \begin{zed}
   STOP \defs \lang \rangl \\
   CHAOS \defs  \power (\seq EVENTS)
   \end{zed}

   \begin{axdef}
   \_ \detchoice \_, \_ \nondetchoice \_ : (TRCSP \cross TRCSP) \fun TRCSP
   \where
   ...
   \end{axdef}

Tho' I should add that this is an example of how Z may be used to support the
mathematical reasoning required in applications of CSP.  It's not an example
of how Z and CSP can be used together in the description of a real-time
system.  

And then we hear from Julian.Rose@bristol.ac.uk ("Julian Rose")

  For my own penny's worth, no-one seems to have highlighted
  the different levels of abstraction between Z and CSP(-like
  languages). Z is about 'whats' and CSP is (mostly?) about
  'hows' and there is a difference. I think Jim Davies hinted
  this when he said "...using CSP to specify the patterns of
  communication between system components, and then Z to specify
  the computational aspects of the components themselves",

which helps to make the point---although I should say that trace and refusal
specifications are 'whats' not 'hows'---that Z and CSP can be used together to
tackle different aspects or concerns in the specification and development of a
real-time system.  The business about 'whats' and 'hows' might be easier to
fathom if you see the process algebra part of CSP as an abstract
implementation language, and the language of traces and refusals as
specifications... SAT is a refinement relation.  

In using Z and CSP together, we would be refining Z --> computational code
within modules or components, and refining CSP specifications --> CSP language
--> communication code or interface designs.  If you see what I mean... 

Jim

--