[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: P.H.Welch@xxxxxxxxx (phw)*Subject*: Re: Re. Lamport / Composition*From*: Adrian Lawrence <adrian.lawrence@xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx>*Date*: Mon, 25 May 1998 22:57:41 +0100 (BST)*Cc*: adrian.lawrence@xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx, paul@xxxxxxxxxxxxxxxxxx, P.H.Welch@xxxxxxxxx, occam-com@xxxxxxxxx*In-reply-to*: <199805220938.KAA02460@xxxxxxxxxxxxx> from "phw" at May 22, 98 10:38:38 am

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

**References**:**Re. Lamport / Composition***From:*phw

- Prev by Date:
**Re: Lamport and toy languages** - Next by Date:
**Re: Lamport "The Temporal Logic of Actions"** - Previous by thread:
**Re. Lamport / Composition** - Next by thread:
**Toy languages** - Index(es):