论文部分内容阅读
随着程序设计的研究与发展，程序的正确性、可靠性、可维护性等问题受到普遍关注，所以对程序规范与验证的形式化方法研究有重要的意义。目前，形式化方法的语义研究大致分为四个分支：操作语义、指称语义、公理语义和代数语义[1]，其中公理语义以程序逻辑为基础，利用最弱(宽容)前置条件(wp，weakest precondition；wlp,weakest liberal precondition)和不变式可以证明程序的部分正确性和完全正确性，基于此，我们采用公理语义来证明面向对象程序设计语言的正确性、可靠性和可维护性。
本文首先在介绍形式化方法和公理语义的基础上，指出了Hoare规则和对象不变式在证明程序部分正确性和完全正确性中的重要作用；其次，我们利用Hoare规则和对象不变式，类不变式，静态数据成员的状态和实例数据成员的状态明确给出了类的公理语义。本文以C＃语言为背景，重点讨论了类的的公理语义，同时也给出了相关的语言成分的公理语义。主要工作包括：
(1)给出了类的公理语义，包括类的声明、类的静态方法、构造函数的公理语义以及类的数据成员访问表达式的公理语义。
(2)给出了与对象相关的公理语义，包括对象的创建，实例方法调用的公理语义。
(3)给出了异常相关的公理语义，包括break，continue等语句的公理语义。
(4)给出了委托、结构、接口等相关的公理语义。