Concurrent object composition in CafeOBJ
Shusaku Iida, Michihiro Matsumoto, Răzvan Diaconescu, Kokichi Futatsugi, Dorel Lucanu · 1998
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. 1 Introduction The principle of "divide and conquer" seems to be the only effective principle in the development of large and complex systems. A system is divided into several independent components and each component is developed independently, after that the system is composed from the already developed components. In general this "divide and conquer" principle is applied recursively. Object-oriented modelling is widely used to support this...