Concurrent Object Composition in CafeOBJ (abstract)
A new method is introduced to concurrently compose an object from
already verified objects.
The most important new feature of our method is that the
verification of the composed object can be done by re-using the
verifications of component objects. That is, the verification of
composed object is also composable. This is not always true. We can
show this can be achieved under some practically reasonable
restrictions.
These can be made possible by using a new algebraic specification
language CafeOBJ which has clear and precise algebraic semantics.
full
paper (draft) -- 105K.
Back to CafeOBJ Home Page