Re: Re design & checking tools

[Bryan Scattergood <bryan@xxxxxxxx>]

Ruth Ivimey-Cook wrote:
> I'm not good enough with CSP to answer this: would it be at all possible to
> automatically translate a compilable occam program into it's CSP equivalent?
> 
> I believe if this were possible, it would have two benefits:
> 
>  1. A programmer used to 'normal' programming languages would be able to
> see how CSP relates to their occam input, which will benefit them immensely
> in understanding CSP.
> 
>  2. CSP models can be practially deriver for programs which were produced
> without a CSP basis, so the CSP can then be examined to check various
> properties, extend the program etc,.

It is almost certainly possible to automatically translate from occam
into CSP, but the resulting models are not useful IMHO. Since CSP is,
to a first approximation, occam-without-assignment the translation can
either discard variables or explicitly model them as parallel
processes. The first loses too much detail, while the latter gets
bogged down in managing access to the 'variables', especially reading
state out of them before evaluating expressions.

For 1, the former translates the coarse structure of the occam, but
discards the familiar 'normal' programming constructs such as loops
and assignments. The latter produces a model which has the same sort
of relation to the occam as the assembly output from a compiler.

For 2, the models are either too abstract to be useful, or too large
for the current generation of CSP tools (except possibly Jeremy's, but
it would make more sense to drive that directly from the occam.)

> If this transform is possible, what about producing skeleton-occam from
> CSP? [that is, producing the bare bones of a program which must be filled
> with the abstracted-out detail later]

Going from CSP to occam requires either constraining the CSP to avoid
multi-way synchronisation (as in Scott's paper at Como) or a
sophisticated translation. In either case the potential user base of
such a tool is limited to CSP-fluent users who wish to target occam.

     Bryan