Hi Peter, I think I can now supply the missing link between the intermediate representation of a JCSP channel, that was verified by FDR, and a pure CSP channel. It came to me while watching cricket this afternoon. The correctness of the JCSP channel depends on the fact that the JCSP implementation offers a slightly restricted form of CSP to the programmer. For the moment let us consider `ALT-free' JCSP networks that use only 1 to 1 channels and no alternation statements. Define a JCSP network as a special kind of parallel CSP network P1 || P2 || .. || Pn, where each Pi is a JCSPPROCESS. JCSPPROCESSS = SKIP | a!x -> JCSPPROCESS | a?x -> JCSPPROCESS(x) | JCSPPROCESS |~| JCSPPROCESS | JCSPPROCESS ; JCSPPROCESS A usage rule is enforced which is that each channel a is used by exactly one process Pi for input and exactly one process Pj for output, i.e. the network is triple-disjoint. (There will be other external events though to represent things like reading in data and printing out results). So we have described the set of CSP processes that we would like to model using JCSP. However we don't really have any CSP channels available for use - we only have JCSP channels, which behave like extra parallel processes. JCSPCHANNEL(a) = (LEFT(a) || RIGHT(a)) / {a} where LEFT(a) = write.a?x -> a!z -> ack.a -> LEFT(a) and RIGHT(a) = ready.a -> a?x -> read.a!x -> RIGHT(a) (This representation of a JCSP channel has been proven correct using FDR) We would like to show that if we take some JCSP network V = P1||..||Pn and transform it in some way that replaces all the CSP channels with JCSP channel processes, then the external behaviour of the program is preserved. Let us define the transformation as follows: Suppose that network V originally contains a CSP channel a, which is written to by process Pi and read from by process Pj. To replace CSP channel a in V we introduce an additional parallel process JCSPCHANNEL(a), and we transform process Pi to Pi' by replacing all occurences of a!x -> Process by write.a!x -> ack.a -> Process and we transform process Pj to Pj' by replacing all occurences of a?x -> Process(x) by ready.a -> read.a?x -> Process(x) Now, because of the nice algebraic laws of CSP, if we can show that the external behaviour of subnetwork Pi || Pj is unchanged by this transformation then it follows that there is no effect on the external behaviour of the network as a whole. What we actually need to prove is that (1): (Pi || Pj) / {a} = (Pi' || JCSPCHANNEL(a) || Pj') / {write.a, ack.a, a, ready.a, read.a} So let's start with the RHS (Pi' || JCSPCHANNEL(a) || Pj') / {write.a, ack.a, ready.a, read.a} = (Pi' || ((LEFT(a) || RIGHT(a)) / {a}) || Pj') / {write.a, ack.a, ready.a, read.a} = (Pi' || LEFT(a) || RIGHT(a) || Pj') / {a, write.a, ack.a, ready.a, read.a} = ( ((Pi' || LEFT(a)) / {write.a, ack.a}) || (RIGHT(a) || Pj') / {ready.a,read.a} ) / {a} So we can establish result (1) if we can prove the following: (2) (Pi' || LEFT(a)) / {write.a, ack.a} = Pi and (3) (RIGHT(a) || Pj') / {ready.a,read.a} = Pj Let us consider the validity of equation 2. This would not hold true in general for any CSP process Pi. But due to our restriction on the syntax of JCSP processes, we can see that it is true as follows. (i) In moving from Pi to Pi' we replace a!x -> PROCESS with write.a!x -> ack.a -> PROCESS (ii) The effect of putting LEFT(a) in parallel with Pi' is then to replace write.a!x -> ack.a -> PROCESS in Pi' with write.a!x -> a!x -> ack.a -> PROCESS (iii) The effect of hiding {write.a, ack.a} is to set write.a!x -> a!x -> ack.a -> PROCESS back to a!x -> PROCESS, which is what we started with. (I think this is the only bit which makes use of the restricted syntax.) Equation 3 is proved similarly and we conclude that the transformation to replace CSP channel `a' with JCSPCHANNEL(a) has not affected the behaviour of the network if the channel is concealed. Having applied a transformation to replace one CSP channel `a' with a JCSP channel we can repeat the step on other channels until only JCSP channels remain. (This is because the transformation from Pi and Pj to Pi' and Pj' preserves the restriced syntax of the JCSP processes). Finally we will have shown that (P1 || .. || Pn) / {a1, .., an} = ((P1' || .. || Pn') || (JCSPCHANNEL(a1) || .. || JCSPCHANNEL(an)) / {write.a1, ack.a1, ready.a1, read.a1, .., write.an, ack.an, ready.an, read.an} Which means that the external behaviour of the network (i.e its behaviour when all internal channels are concealed) is exactly preserved. So we are then perfectly safe to reason about JCSP programs in their natural form without the additional baggage of LEFT/RIGHT process pairs for each channel. I am confident that this proof can easily be extended to take care of alternation, to establish the full correctness of JCSP. Jeremy ------------------------------------------------------------------------- Dr J. M. R. Martin Oxford Supercomputing Centre Tel: (01865) 273849 Wolfson Building Fax: (01865) 273839 Parks Road Email: jeremy.martin@comlab.ox.ac.uk Oxford OX1 3QD WWW: http://users.ox.ac.uk/~jeremy