摘要
Object-Z是形式规格说明语言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.
出处
《计算机科学》
CSCD
北大核心
2006年第7期230-232,256,共4页
Computer Science
基金
国家自然科学基金(60373072)
上海市教委第四期重点学科建设基金资助
