Re: Re. Lamport / Composition

[Adrian Lawrence <adrian.lawrence@xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx>]

phw writes:
> 
> 
> and he quotes the abstract from Lamport's technical note:
> 

> There's a lot I don't understand in the paper -- well, most of it I'm
> afraid :-( ...  A simple problem is used for illustration (a clock showing
> hours and minutes and a railway station with one of these clocks and
> a signal that changes colour from time to time).  But the mathematics
> that goes with it is not for the faint-hearted, and that certainly includes
> me :-( ...
> 
> There's no reference to CSP in the paper, so this is a challenge for
> the Oxford people.  Any chance of a CSP specification and verified design
> that implements his examples?

I have just turned up one of Lamport's references. Indeed, it seems to
be the foundation for the technical note. ACM Prog Lang & Sys, v16,872, 1994
"The Temporal Logic of Actions". The Introduction is very revealing.
He contrasts "real" and "toy" languages. You can reason about "toy"
languages, but "real" languages are needed in practice. I really wonder if
he knows *anything* about occam? I/we would say that occam has all/(most of)
the desirable properties of "toy" languages, while also being practical.
Yes he talks about referential transparency - without using the term;
aliasing; side effects; functions; and the fact that "C has no primitives for
sending messages across wires".

His "Comparison with Related Formalisms" makes no mention of occam or CSP!

I am really surprised that someone of Lamport's stature seems to have a 
blind spot. Or maybe he regards the whole approach as unworthy of
mention. But I haven't read the whole article, so I may have got this
wrong and being unjust.

Far from attacking the occam approach, the article is providing excellent
reasons in favour. I have yet to get to grips with temporal logic
proper, but I think I regard it as a complementary approach providing elegant
formulations of certain aspects of system design.

Adrian
-- 
Adrian Lawrence.
adrian.lawrence@xxxxxxxxxxxxxx or adrian.lawrence@xxxxxxxxxxxxxxx
  MicroProcessor Unit        | Computing Laboratory,
  13, Banbury Road,          | Wolfson Building,
  Oxford. OX2 6NN.           | Parks Road, Oxford.
  UK.                        | OX1 3QD. UK.
Voice: (+44)-1865-273274,(+44)-1865-283526  Fax: (+44)-1865-273275