Reasoning about Polymorphic Behavior in Object-Z
基于Object-Z多态推理

Object-Z is an extension to the formal specification language Z,which facilitates specification in an object-oriented style and thus has object-oriented characteristics.It improves the clarity of large specifications through enhanced structuring.Class and its relationship construction technology in Object-Oriented method(OO)are apt to describe large-scale and complicated system with Object-Z,based on mathematics logic and set theory,thus we can reason about its formal specification.One of the most important ideas underlying the object-oriented approach is polymorphism.This paper discusses how to reason about the polymorphic behaviors in Object-Z and presents its inference rule.With our approach,we can reason about the specific behaviors of subclass objects.Moreover,we take into account the reuse of reasoning emphatically.