[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Re. Lamport / Composition
phw writes:
>
>
> > Compositional reasoning about a system means writing its
> > specification as the parallel composition of components and
> > reasoning separately about each component. When distracting
> > language issues are removed and the underlying mathematics
> > is revealed, compositional reasoning is seen
> > to be of little use.
If this continued "for reasoning about C and similar languages." which I
think is implied, then we don't have a problem with that? This is really
what you said in your original reply.
> Well, I downloaded the technical note and stared at it over lunch with
> my colleagues David Wood and Jim Moores. It's heavy into mathematical
> logic and has certainly got something against capturing abstractions
> in programming languages and reasoning about them at that level. He
> says proofs must be reduced to pure logic -- constraining yourself to
> some programming abstraction is too awful.
>
> 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 :-( ...
Well, I have read a bit more of his original Temporal Logic paper which
seems to be essential to follow the technical note. I found the
definitions of several terms that floored me there. As far as I can see,
his temporal logic is a just a subset of HCSP. He is entirely concerned
with assignment and state transformations. He even introduces traces
but calls them "behaviours". Not to be confused with behaviours in HCSP.
So again, he seems to be unfamiliar with modern CSP, otherwise I would have
expected him to use the term "trace" or at least mention the correlation.
There is no concept of a general event: just actions which are pretty much
state transformations. In HCSP we have general events, some of which
may be associated with state changes. He has a few new (well old since
temporal logic has been around since 197?) logical operators, and maybe they
allow concise descriptions of some properties. But there seems to be
nothing here which is radically different from CSP foundations. Just
a bit more restricted.
But any experts on temporal logic listening? Are my impressions correct?
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