Re: Re. Lamport / Composition

[Adrian Lawrence <adrian.lawrence@xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx>]

Lamport: "Composition: A Way to Make Proofs Harder"
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 

Now that I have  skimmed through the background paper, I
can at least follow the temporal logic examples in the above.
I will need to find some more time to gets to grips with his
arguments about compositionality. Much of what he says about mathematics
as opposed to programming languages matches our philosophy.
Yet I recognise little of his description of CSP:
   "We call such a language a pseudo-programming
    languages (PPL). Some PPLs, such as CSP, use constructs of ordinary
    programming languages."
I suppose that has a some truth in it, although using refinement for
specification does not seem to be addressed. And Jeremy may have something
to say about "sat"isfying predicates when he has some spare time.
But Lamport sees the jump between mathematics and "real" languages as
a unsolved problem. That is where we have a full solution. We have a 
rigorous route between implementation and mathematical specification.
And I think that Lamport says that the languages themselves will and must
be compositional. And he says of course that the mathematics itself
is also compositional. 

As I have noted before, his  model of the universe by a state mapping seems
a bit restrictive. His model also is incapable of expressing true 
concurrency. But they may be just artifacts of a particular instance.

He mentions in the earlier paper the problems of structuring large
mathematical documents. Surely the whole essence of Z is its use of
schemas to modularise and structure large arguments. But it gets no
mention.

Has anyone else understood the main argument? I need to think about
fairness and liveness in his sense. Just now, I am not very clear why
his "stuttering" cannot be handled with hiding. But that just demonstrates
that I don't really understand his system as present.

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