Formalizing UML/OCL Multiple Inheritance with FoCaLiZe

Multiple Inheritance is an Object Oriented feature that is widely adopted by the Unified Modeling Language (UML). To generate software from a UML model, programming languages that supports multiple inheritance (such as C++, Eiffel or POOL) are available. But, when it is necessary to check and analyze model properties, it is relevant to use formal methods (environments) that help developers to specify and check such properties. In this paper, we propose a formal transformation of UML multiple inheritance into FoCaLiZe, a formal programming environment using a proof-based approach. The transformation naturally captures multiple inheritance of classes attributes, methods and OCL constraints with methods overriding and late binding mechanisms. This transformation enables to specify theoretical and critical systems properties. In addition, it is possible to check and prove such properties using the automatic theorem prover of FoCaLiZe.