Re: CSP questions

I have been pursuing references to CSPP and HCSP, brainchildren of Adrian E. Lawrence, which sound like they may have some of what we need for formal verification (though I have not fathomed his notation). But I cannot trace Dr. Lawrence’s work past 2006, and I cannot find any reference to it in Roscoe, Theory and Practice of Concurrency. Can anyone give me further direction on this?

On Mar 7, 2017, at 1:25 PM, Larry Dickson <tjoccam@xxxxxxxxxxx> wrote:

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

On Feb 14, 2017, at 4:42 PM, Larry Dickson <tjoccam@xxxxxxxxxxx> wrote:

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