| 摘要 | 第1-5页 |
| Abstract | 第5-9页 |
| 引言 | 第9-12页 |
| 1形式化方法及公理语义 | 第12-30页 |
| ·形式化方法 | 第12-14页 |
| ·公理语义 | 第14-18页 |
| ·公理语义的完全正确性 | 第18页 |
| ·与异常有关的语句的公理语义 | 第18-25页 |
| ·if语句的公理语义 | 第19-21页 |
| ·return语句的公理语义 | 第21-22页 |
| ·带标号语句的公理语义 | 第22-23页 |
| ·continue语句的公理语义 | 第23页 |
| ·break语句的公理语义 | 第23-24页 |
| ·语句和语句块的公理语义 | 第24-25页 |
| ·Java的异常处理机制的公理语义 | 第25-30页 |
| ·Java的异常处理过程 | 第25-26页 |
| ·Java中异常处理的分类 | 第26页 |
| ·throw语句的公理语义 | 第26页 |
| ·try-cathc语句的公理语义 | 第26-28页 |
| ·try-catch-finally语句的公理语义 | 第28-30页 |
| 2类和对象的公理语义 | 第30-46页 |
| ·类定义的语法 | 第30-31页 |
| ·类定义的具体例子 | 第31-34页 |
| ·记号 | 第34-36页 |
| ·类的声明语义 | 第36-37页 |
| ·语法 | 第36页 |
| ·语义 | 第36页 |
| ·公理语义 | 第36页 |
| ·说明 | 第36-37页 |
| ·应用于本节2中的例子 | 第37页 |
| ·静态方法的公理语义 | 第37-38页 |
| ·语法 | 第37页 |
| ·语义 | 第37页 |
| ·公理语义 | 第37-38页 |
| ·说明 | 第38页 |
| ·应用于2中的例子 | 第38页 |
| ·构造函数的公理语义 | 第38-40页 |
| ·语法 | 第38-39页 |
| ·语义 | 第39页 |
| ·公理语义 | 第39-40页 |
| ·对象创建表达式语义 | 第40-42页 |
| ·语法 | 第40页 |
| ·语义 | 第40页 |
| ·公理语义 | 第40-41页 |
| ·说明 | 第41页 |
| ·应用于2中的例子 | 第41-42页 |
| ·实例方法的公理语义(此处未考虑多态情况) | 第42-43页 |
| ·语法 | 第42页 |
| ·语义 | 第42页 |
| ·公理语义 | 第42页 |
| ·说明 | 第42页 |
| ·应用于2中的例子 | 第42-43页 |
| ·域访问表达式 | 第43-46页 |
| ·语法 | 第43页 |
| ·语义 | 第43-44页 |
| ·公理语义 | 第44-46页 |
| 3与数组相关的表达式的公理语义 | 第46-53页 |
| ·数组实例创建表达式的公理语义 | 第46-48页 |
| ·语法 | 第46页 |
| ·语义 | 第46-47页 |
| ·公理语义 | 第47-48页 |
| ·数组访问表达式的公理语义 | 第48-53页 |
| ·语法 | 第48页 |
| ·语义 | 第48页 |
| ·公理语义 | 第48-50页 |
| ·举例说明 | 第50-53页 |
| 4多态性的公理语义 | 第53-63页 |
| ·继承和多态性的公理语义描述 | 第53-54页 |
| ·面向对象和非面向对象的公理语义 | 第54-57页 |
| ·Java语言的方法正确性证明框架 | 第57-63页 |
| 结论 | 第63-64页 |
| 参考文献 | 第64-67页 |
| 攻读硕士学位期间发表学术论文情况 | 第67-68页 |
| 致谢 | 第68-69页 |
| 大连理工大学学位论文版权使用授权书 | 第69页 |