Re: Re design & checking tools

[Ruth Ivimey-Cook <ruthc@xxxxxxxxxxxxxxxxxx>]

At 13:15 22/04/99 +0100, Bryan Scattergood wrote:
>Ian East wrote:
>> Surely this has to do just with degree of abstraction. The only reason 
>> for considering a single state for each state value (eg with an INT32) is 
>> if the process behaves differently with regard to others according to 
>> every distinct case (0, 1 , 2 etc). This is rarely true.
>
>This sort of abstraction is usually obvious to a human, but as Jeremy
>said, it is hard to automate. The same work is involved in producing
>(say) a tractable CSP model of an existing implementation, but that
>currently requires a competent CSP user and is tedious and
>error-prone.


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,.

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]

Regards,

Ruth