| Hello all, We need to learn about formal verification, so I started with Martin and Jassim, “Technique for Checking the CSP sat Property”, WoTUG-21, poked at Roscoe, Theory and Practice of Concurrency, Prentice-Hall, and wound up at Roscoe and Hoare, “The Laws of OCCAM Programming,” Theoretical Computer Science 60 (1988) 177-229. A couple of questions on the last. (1) In (5.6)* and (5.7)*, p 187, the c?x and x:=e instructions seem to share x across PAR members. Am I right that x is only a general symbol so that this illegal sharing does not really take place? (2) The WHILE combination (W.2), p 221 and 228, seems incorrect: If I type v for OR, ^ for AND, and T for DIVERGENCE it claims WHILE b1 (WHILE b2 P) = WHILE b1 v b2 IF(b2 P, true T) But this clearly seems wrong if b1 is FALSE and b2 is TRUE. I thought at first that the v was a typo for ^ but ^ only works if you require b1 and b2 to be constant. If they both start TRUE and one turns FALSE in the course of P, the equality fails. Is there further work on occam 2 or later occam along this line? Larry Dickson |