[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Re. Lamport / Composition
> 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.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