Java语言的类和多态性的公理语义

论文摘要

本文以Java语言为背景,重点讨论了类的继承和多态性的公理语义,同时也给出了必要的及相关的语言成分的公理语义。主要工作包括:（1） 给出了类的公理语义,包括类的声明、类的静态方法、构造函数的公理语义以及类的数据成员访问表达式的公理语义。（2） 给出了与对象相关的公理语义,包括对象的创建,实例方法调用的公理语义。（3） 数组也是对象,我们给出了与数组相关的公理语义,包括数组实例创建表达式和数组访问表达式的公理语义。（4） 因为类的继承和多态性是面向对象程序设计语言的一种机制,而非一种语言成分,故以不同于上述三类语言成分的方式描述它们的公理语义。随着程序设计的研究与发展,程序的正确性、可靠性、可维护性等问题受到人们的普遍关注。许多程序规范与验证的形式化方法涌现出来,对程序设计方法学的发展起了积极的推动作用。但是尽管面向对象的方法在今天的软件开发中得到广泛应用并取得显著的成就,这个领域的形式化正确证明方法仍然是-个难以解决的问题。在正确性证明中最广泛应用的方法是Hoare方法,它利用推导公式来描述程序或程序片断的输入/输出关系。对象不变式描述了面向对象数据结构中元素间的关系,在对象创建后以及方法引用前后它总为真。对象不变式在面向对象程序的证明中具有重要作用。利用对象不变式,类不变式,静态数据成员的状态和实例数据成员的状态,并结合Hoare公理系统,我们明确给出了类的公理语义。多态性是面向对象程序设计的-个重要特点,也是难点,在使用时最容易发生错误和误解。在用公理语义描述多态性的时候,由于我们使用的描述方法是静态的,而被描述对象是动态的,所以在描述多态性的时候需要做大量工作。本文通过引入新的谓词和函数确定了用公理语义描述多态性的前置条件和后置条件,从而描述了多态性的公理语义。利用我们给出的公理语义可以用于编译、解释Java程序的生成;验证用Java语言编写的程序的正确性。

论文目录

• 摘要
• Abstract
• 引言
• 1形式化方法及公理语义
• 1.1形式化方法
• 1.2公理语义
• 1.3公理语义的完全正确性
• 1.4与异常有关的语句的公理语义
• 1.4.1if语句的公理语义
• 1.4.2return语句的公理语义
• 1.4.3带标号语句的公理语义
• 1.4.4continue语句的公理语义
• 1.4.5break语句的公理语义
• 1.4.6语句和语句块的公理语义
• 1.5Java的异常处理机制的公理语义
• 1.5.1Java的异常处理过程
• 1.5.2Java中异常处理的分类
• 1.5.3throw语句的公理语义
• 1.5.4try-cathc语句的公理语义
• 1.5.5try-catch-finally语句的公理语义
• 2类和对象的公理语义
• 2.1类定义的语法
• 2.2类定义的具体例子
• 2.3记号
• 2.4类的声明语义
• 2.4.1语法
• 2.4.2语义
• 2.4.3公理语义
• 2.4.4说明
• 2.4.5应用于本节2中的例子
• 2.5静态方法的公理语义
• 2.5.1语法
• 2.5.2语义
• 2.5.3公理语义
• 2.5.4说明
• 2.5.5应用于2中的例子
• 2.6构造函数的公理语义
• 2.6.1语法
• 2.6.2语义
• 2.6.3公理语义
• 2.7对象创建表达式语义
• 2.7.1语法
• 2.7.2语义
• 2.7.3公理语义
• 2.7.4说明
• 2.7.5应用于2中的例子
• 2.8实例方法的公理语义（此处未考虑多态情况）
• 2.8.1语法
• 2.8.2语义
• 2.8.3公理语义
• 2.8.4说明
• 2.8.5应用于2中的例子
• 2.9域访问表达式
• 2.9.1语法
• 2.9.2语义
• 2.9.3公理语义
• 3与数组相关的表达式的公理语义
• 3.1数组实例创建表达式的公理语义
• 3.1.1语法
• 3.1.2语义
• 3.1.3公理语义
• 3.2数组访问表达式的公理语义
• 3.2.1语法
• 3.2.2语义
• 3.2.3公理语义
• 3.2.4举例说明
• 4多态性的公理语义
• 4.1继承和多态性的公理语义描述
• 4.2面向对象和非面向对象的公理语义
• 4.3Java语言的方法正确性证明框架
• 结论
• 参考文献
• 攻读硕士学位期间发表学术论文情况
• 致谢
• 大连理工大学学位论文版权使用授权书