Final Semantics of Object Behavioral Equivalence

Behavioral equivalence is an important issue in the researches of dynamic substitutability for objects and it is still difficult to verify it effectively and precisely. In this paper, we use co algebras to formally describe abstract classes, classes and objects, among which their behavioral structures are depicted parametrically with strong monads. Each class specification is defined as the compositions of functors and assertions. Classes are regarded as co algebraic models satisfying some class specification, and objects belonging to a class are viewed as elements in the state space of the class. After that, we use final co algebras to discuss object behavioral equivalence wrt the same and different class specifications, as well as giving their interpretations under different structures of strong monads. Finally, examples are taken to illustrate how to use PVS tools for verifications.