Lamport and toy languages

[Adrian Lawrence <adrian.lawrence@xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx>]

Lamport & toy languages  "The Temporal Logic of Actions"
~~~~~~~~~~~~~~~~~~~~~~~

Lamport's first sentence is
 "A concurrent algorithm is usually specified with a program".
2 paragraphs on he says
 "How can we abandon *conventional* programming languages in favour of logic
if the algorithm must be coded as a program to be executed?"
(My emphasis.)

His whole point is that conventional languages are hopelessly broken and
trying to reason about their properties is next to impossible, especially
concurrent properties. His solution is to express both specification and
algorithm mathematically, in his case in a (temporal) logic.

In the occam community, we would not dream of specifying an algorithm in
a conventional language, would we? We would probably use either

1) a Z specification;
2) a CSP specification;
3) an occam program;
4) or something else mathematically based.

Lamport completely misses the fact that we already have a programming
language in which reasoning is possible and mathematically based,
although he does mention and dismiss declarative languages later in the
article.[Even occam is a bit complicated, but we can abstract away
to a simpler CSP view. After all, occam has to carry all the baggage
necessary to program real machines and all the type checking need for
practical programming. And the translation occam <--> CSP is straightforward
because they share the same rigorous semantics.]

More from Lamport:-
"But, why replace a programming language by logic? Aren't programs simpler
than logical formulas? The answer is no. "
He then enters into a discussion of assignment contrasted with the
= relation, aliasing, and mathematical versus conventional language
"functions".

His temporal logic, or at least the semantic model, is based entirely
on state. State being a mapping Names -> Values. And actions which
are state transitions, using a Z-like new' = f(old): decoration is used
as in a \Delta schema. There is no notion of event other than these state
changes as in CSP. So it would be tricky to describe external interaction
without ascribing external state? As far as I can see, despite the 
term "temporal" logic, there is really *no* proper treatment of time.
It is rather like untimed CSP: all that is modelled is sequence, and that
in a very abstract way. 
I am not sure yet, but I think that his model as it stands can only deal
with shared memory...

With CSP, TCSP and HCSP we have a far more powerful system. Of course
having more power *can* sometimes make things more complex. But as far
as I can see just now, the CSP family descriptions are just as simple.
Maybe there are some things that temporal logic will capture more
elegantly: that wouldn't be surprising.

So we can agree with everything that Lamport says: we just wish that he
might have mentioned the CSP family. 

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