🚀 go-pugleaf

In reply to J. Song (of York)

| Combining Z and CSP means that you can have either states or events in the
| language, which are sometimes useful.

It is not possible to combine Z and CSP in a simple way because they
have different underlying mathematical structures. People are talking
about using them as complementary notations.

| 	But I wonder why we cannot define concurrency operators, trace,
| process by using Z and then use these highlevel constructs to define
| concurrent systems.

Brendan Mahoney suggested his description of traces. For processes
you might be able to define a syntactic relation, ||, for example, but
you will need to embrace the semantic model of CSP to describe it.

| In fact B. Sufrin and Jifeng He have already made some
| efforts on this [the high level constructs].

I think the same authors had a publication in volume 1 of the BCS FAC
journal. There, they advanced a Z specification by a process of refinement,
if I remember correctly (correct me if I'm wrong).

In general, refinement is the kind of approach required to advance a Z
specification into a process-based one, like CSP. Someone pointed out to me
work on action systems (originally by R.J.R. Back), that attempt a
sort of refinement, some papers are published in the FAC journal.

Julian