| Larry
In Hoare’s Communicating Sequential Processes (Prentice-Hall, 1985) SKIP is introduced in Chapter 5 (Sequential Processes) and Section 5.2 gives some Laws.
L1 is SKIP; P = P; SKIP = P
I can’t see a straightforward statement of PAR(P, SKIP) = P but I suspect it can be derived by a transformation of the form
PAR (P, SKIP) = ALT (P;SKIP, SKIP;P) = ALT (P, P) = P with suitable care (at least with alphabets and output guards)
Roger
Thank you to everyone who communicated personally with me on the 14 Feb post. Here is an even more elementary question relating to Roscoe and Hoare, “The Laws of OCCAM Programming.”
Perhaps these are considered too trivial to require a law. But I searched and could not find the following, or anything that implied them:
PAR(P, SKIP) = P SEQ(SKIP, P) = P SEQ(P, SKIP) = P
Larry 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
|