论文部分内容阅读
Object-Z是形式规格说明语言Z的面向对象扩充，基于严格的集合论与数理逻辑，具有面向对象的特点：类、对象、继承、封装与多态等。用它可以精确描述大型软件需求规格说明，且能够进行严密的逻辑推理与验证。本文主要探讨了它的多态性推理，给出了相应的推理规则与方法，可以推理出Object-Z的多态行为，并着重体现推理的重用。