为了解决软件体系结构漂移和体系结构侵蚀的问题,英国艾塞克斯大学的Eden博士从理论上提出了一种新的程序设计范型——两层式程序设计(TTP).通过对该理论的研究以及对传统程序编译器的思考,本文提出了一种新的方法用于构建设计模式的形式化验证工具.该工具从概念上分为两层,第一层为传统编译层;第二层为编译扩展层,该层使用传统编译层的信息对程序进行设计模式的形式化验证.在编译扩展层中,同时考虑了程序的内部抽象表示、连接映射的内部表示以及设计模式规格说明的内部表示,这样就提高了工具的灵活性和可扩展性.在对设计模式形式化验证之前,需要经过设计模型生成、设计模式规格说明解释两个步骤,本文主要对这两个方面以及设计模式的形式化验证策略进行了研究及探讨.以此为基础,本文作者用面向对象的方法设计并实现了TTP环境中的设计模式验证工具DPV_TOOL(Design Pattern Verification Tool),其中的第二层规格说明使用Eden博士提出的设计模式形式化描述语言LePUS.论文工作主要有以下几方面:1.通过对Java语言的具体分析,根据Eden提出的设计模型定义,研究了Java语言的设计模型表示法,它是设计模型生成的参照标准.此外,还对LePUS规格说明和连接映射的正规文法进行了研究,这是设计模式规格说明解释的参照标准.2.设计了工具的概念框架,并以此为基础设计和实现了DPV_TOOL.此外,研究了新框架中的内部数据结构和验证算法设计.3.应用DPV_TOOL对两个经典的设计模式Factory Method和Template Method进行验证,并对验证结果进行了分析.通过实例表明了所完成的研究、开发和实现工作的可行性、正确性和有效性.LePUS是设计模式形式化工作中一个富有意义的尝试,LePUS的优点在于集合变量的表达和推理能力,但它尚处于发展完善中.TTP是软件工程领域中一个全新概念,Eden博士领导的工作组也正在进行TTP支持环境的研究开发,曾预期在2003年9月完成一个原型.本论文及其相关工作独立地从一个方面表明了LePUS和TTP在设计模式形式化中的意义和作用.