From: A E Lawrence (adrian.lawrence_at_email.domain.hidden)
Date: 2000-10-17 20:55:12
"Campbell, John" wrote:
>
> So, here it is: Can CSP be augmented to prove the absence
> of open-ended memory requirements the same way it can
> show the absence of deadlock? Outlawing aliasing seems
> heavy handed. But if you can show (prove) that allocations
> have a limited lifetime, it would mean that the garbage collector
> will never be invoked. -jc
Standard CSP doesn't really model memory in the usual sense. You can
model memory if you wish, but as a sort of hardware emulation. There is
a notion of state in the sense that a process can depend on a
(declarative) variable.
In order to capture the assignment aspects of occam, I added the idea of
special events with side effects on memory into HCSP.
I don't see why CSP would help you model memory requirements, but there
might be work on this somewhere. Even with "assignment events" in HCSP,
one would use other formal approaches to model the memory evolution,
although I suppose traces might help a litlle.
Adrian
-- Dr A E Lawrence
This archive was generated by hypermail 2.1.7 on 2004-10-31 20:03:55 GMT
© Copyright WoTUG
All rights reserved