随着社会各领域需求的不断增加，计算机软件系统的规模日益庞大，结构也越来越复杂。这一方面促进了软件开发中面向对象(OO)技术的快速发展，如设计模式、框架应用等重要程序设计技术已被成熟地用于提高软件的质量;另一方面对安全攸关的软件系统的可信度提出了更高的要求和挑战。应用形式化方法验证OO程序可靠性的研究工作已取得很多成果，但已有理论成果能够支持的OO特性还远落后于OO技术的发展和在软件系统开发中的实际应用。因此针对复杂软件系统开发中广泛应用的OO特性（如接口类型、抽象、动态绑定等）和设计技术（对象合成使用、框架等），设计适用的形式化描述和验证技术具有重要的意义。另外，为支持OO软件系统开发的模块化和代码复用等重要特点，设计出的规范和验证技术必须具有抽象性和模块性。　　本文以一个典型的OO程序语言模型-μJava（类Java顺序式程序语言）-为研究对象，以一个OO程序的形式化规范和验证的初步框架-VeriJ-为基础，通过进一步研究OO语言的各种主要特性（如对象、类、继承、对象共享、动态绑定、多态、抽象等，）以及它们在OO程序设计中的重要作用，分析它们在OO程序的形式化规范描述和验证工作中引发的复杂问题，提出了相应的处理技术来逐步扩展VeriJ框架。本文还将结合一些典型的OO程序实例包括复杂的数据结构和基于组件系统，讨论新框架在程序正确性证明中的应用，并与已有的相关工作做了对比分析。　　为支持基于接口的OO设计，本文首先将OO的接口类型扩展到语言模型中。基于抽象规范谓词和抽象方法规范概念，本文提出了一个扩展的验证框架VeriJI，它能够抽象地描述基于接口的OO程序的行为规范，并模块化地证明这类程序实现的正确性。VeriJI框架为接口类型提供的抽象规范描述技术，不但彰显了“封装实现细节”、“分离抽象与实现”和“提供多态化实现统一的接口”等接口类型特有的角色，也支持了外部用户程序仅依赖于接口类型信息的证明。　　验证框架VeriJ（和VeriJI）使用的规范谓词技术能够抽象并封装常见的单个数据结构，如链表、栈、队列、树、数学性质等，但还不足以描述更复杂的数据结构，也不能体现多个数据结构间的合成或聚合等交互关系。另外，基于接口类型的用户代码的证明应该只需要使用接口层次的抽象规范，但是VeriJI框架中接口层次提供的抽象规范明显不能满足用户需要。为解决这些问题，本文提出使用公理逻辑断言描述复杂数据结构的性质和多个结构之间的关系。这种公理断言描述在抽象的接口层次，独立于任何实现，但能够全局地为系统的实现提供语义约束。扩展公理概念及相关的规范和验证技术到VeriJI框架中，本文提出了另一个验证框架VeriJA。　　应用VeriJA验证框架，本文为Web应用中广泛使用的模型-视图-控制器(Model-View-Controller，MVC)架构程序设计了一种通用的、形式化规范描述和验证技术，并将其成功地应用到一个实例程序的证明中。　　本文最后总结了工作，并展望了进一步的研究工作，包括单对象和多对象的对象不变式语义、规范描述方式、相关的证明义务和技术，以及我们提出的形式化验证框架在设计模式、框架等程序设计技术中的应用前景。