共代数方法及其在面向对象技术中的应用

摘要

如今面向对象软件开发技术已广泛应用于软件系统的设计与构造，面向对象范型是对客观世界活动的自然刻划，其中的对象是对客观世界中有形或无形实体的直接模拟。作为面向对象系统组织结构的核心，类代表了对象本质的、主要的、可观察的行为。采用面向对象技术开发软件主要好处是，能够减小问题域与解题域之间的语义间隙，使得软件开发过程显得比较自然，从而可提高软件生产率。所以如何评价一个类的实现所能体现出客观概念的完整程度，就成了考察一个类代码实现好坏的关键。 目前计算机辅助阅卷系统在对程序设计问题的评判方面，主要考察程序运行结果的正确性和实现功能的完备性方面，注重对结构化设计思想的考核，而对现在普遍采用的面向对象技术的语义支持不够，没能充分考核学生利用面向对象思想分析问题和解决问题的能力。本论文工作的主要目的就是希望能够在面向对象程序设计的语义分析自动化实现方面进行一些理论和实践方面的探索，尝试利用形式化方法，在语义的层次上分析和验证类的具体实现与客观概念之间的贴近度。 这需要对类进行良好的形式化描述，但目前面向对象范型还没有一个成熟的语义模型。传统的代数方法是从“构造”的角度研究数据类型，而代数的对偶概念—共代数，可从“观察”的角度考察系统及其性质。共代数方法对于研究基于状态的系统有独特的优越性，可以对系统的行为等价、不确定性等从数学上进行深入的探讨。所以本论文采用共代数作为对象系统的语义模型。在本论文中，首先对共代数的基本概念、范畴理论基础、共代数逻辑以及共代数方法在面向对象语义分析中的应用等方面进行了详细的讨论。然后，本文结合形式化方法与类的共代数语义，提出了一个辅助阅卷系统模型，探索利用基于共代数的类规范描述语言CCSL给出某个概念的语义模型，并将其转换成高阶逻辑，最终通过定理证明器PVS验证代码模型的断言正确率，以此来提高辅助阅卷系统对面向对象程序设计语义完整性的评阅性能。