🚀 go-pugleaf

In <JIM.DAVIES.92Aug11180159@pierrot.prg.ox.ac.uk> Jim.Davies@prg.ox.ac.uk (A Wooden Fish on Wheels) writes:



>  * CSP can be used for the specification and analysis of patterns of
>    communication (that's what a CSP process is).  These patterns can
>    evolve concurrently, and timing information is easily included.

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. Indeed any attempt to rigorously treat real-time
issues would benefit from study of this most relevent area of
mathematical endeavour. Afterall it was started by Newton and Liebniz.

>  * Z can be used for the specification and analysis of state-based 
>    or transformational systems.

Z is essentially a machine parsable (formal) version of classical set theory
which has a large body of literature and convention explaining how it may be
used to specify state transition systems. However it is readily
adapted to other fields of endeavour.

>So it seems sensible to use CSP (or something very like it) and Z
>together, using CSP to specify the patterns of communication between
>system components, and then Z to specify the computational (or
>transformational) aspects of the components themselves.

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}

etc

--
When soldiers form lines or hollow squares, you call it reason.
When wild geese in flight take the form of a letter V, you say instinct.
When the homogeneous atoms of a mineral arrange themselves into shapes
mathematically perfect you have nothing to say. You have not even invented a name to conceal your heroic unreason."