分划递推法中泛型约束机制

第1章 绪论 1.1 研究背景 泛型程序设计是指设计程序不仅可以使用数据作参数，还可以使用数据类型、操作、构件、服务和子系统等作参数。1968年，McIlroy等[1]提出可重用软件部件的概念，即像组装硬件部件生产计算机一样组装软件部件生产软件。本书首次提出可重用软件部件要力求泛型(generality)，以应对软件部件规模庞大和正确性验证等问题。20世纪60年代，函数式编程语言LISP采用的高阶函数和参数化多态的编程风格，是泛型程序设计的早期雏形。70年代至今，多态类型系统得以完整实现，其中包括Siek和Milner等[2-4]的工作。80～90年代，Musser等正式提出了泛型程序设计基本方法和原则[5-8]。使用泛型程序设计技术可以大幅度提高程序的可重用性、可靠性和开发效率，使建设软件构件工厂的理想得以实现。C++标准模板库(standard template library，STL)就是典型的成功实例[9]。泛型程序设计被认为是比面向对象程序设计(object oriented programming，OOP)更具影响力的程序设计范型[10，11]，因此引起国际计算机界的广泛重视。 然而，泛型程序设计在提出之后，并没有包含安全语言泛型机制。例如，Ada语言[8]和C++语言[12]均可实现类型和操作参数化，但对于其中的类型参数和操作参数没有实行安全约束机制，这导致在泛型参数实例化过程中无法判断哪些实例类型可以实例化数据类型参数，哪些实例操作可以实例化操作参数。一些本应该在编译阶段发现的语法错误转变成程序运行时才能被系统发现的语义错误，这带来了严重的安全性问题。近年来，泛型约束逐渐成为国际上的研究热点。Java语言在其SE1.5版本之后添加了泛型及其约束机制[13]，对类型参数的约束通过Extends和Implements子句来实现，子句分别说明了类型参数所属的类和实现的接口列表，值类型以打包/解包方式实例化并能得到约束。C#采用了修改虚拟机以支持类型参数化的方案，加入C#2.0及以后版本中[14-16]，C#对类型参数的约束通过Where子句来实现，子句中可以说明类型参数所属的类和实现的接口列表。元语言(meta language，ML)使用了signature[17，18]，Haskell带有type class机制[19，20]，Musser将Concept概念扩展到C++语言，提出基于公理语义的泛型约束机制，并称这种语言为ConceptC++或C++0X[20]。北京大学计算语言学研究所孙斌提出了命名类型约束机制[11]等，均在其各自设计的语言中支持泛型及其约束，但是这些语言的新的泛型约束机制均仅限于类型参数约束，且存在抽象程度不高、不易于形式化验证等不足，严重限制了泛型程序设计方法的应用范围。 1.2 研究内容 分划递推法由PAR方法和PAR平台组成，是江西省高性能计算技术重点实验室软件形式化和自动化学术团队提出并研制成功的一个程序设计环境[21，22]。它由泛型规约和算法描述语言Radl、泛型抽象程序设计语言(abstract programming language，Apla)、形式规约变换规则、系列算法和程序自动转换工具，以及系统的程序设计方法学构成。PAR方法和PAR平台包含循环不变式的新定义和新的开发策略、统一的算法程序设计方法、自动生成SQL查询程序等关键技术，并支持算法程序的形式化开发。文献[23]～[25]证明，用PAR方法提供的语言、变换规则和系列转换工具开发的算法程序具有原理简单、使用方便、通用性强、可靠性高等特点，可以大幅度提高复杂算法程序的生产效率。 Isabelle是一种通用的交互式定理证明器[26]，由英国剑桥大学Lawrence C. Paulson和德国慕尼黑技术大学Tobias Nipkow于1986年联合开发，用函数式编程语言ML来编写，使用自然演绎规则进行定理证明。它既支持数学公式的形式化描述，又为公式的逻辑演算提供了证明工具。Isabelle主要应用在数学定理证明和形式化验证领域，尤其是计算机软、硬件的正确性验证以及程序设计语言和协议的验证等方面。 江西省高性能计算技术重点实验室软件形式化和自动化学术团队在2005年获准的国家自然科学基金面上项目“基于PAR方法和PAR平台的泛型程序设计关键技术研究”(60573080)中，对泛型程序的正确性理论和新的泛型机制进行了深入研究，在提出的泛型算法设计语言Radl和抽象程序设计语言Apla中成功地实现了类型和操作参数的泛型机制，但在这些机制中没有包含安全语言泛型机制，限制了泛型程序设计技术的安全使用。2010年，薛锦云领衔申请获准的国家自然科学基金重大国际(地区)合作交流项目“若干软件新技术及其在PAR平台中的实验研究”(61020106009)将在PAR中实现泛型约束机制作为该项目四大研究目标之一。本书将针对这一研究目标深入开展研究： (1)在PAR中设计抽象约束机制，其*终表现形式为谓词逻辑公式，同时支持语法和语义层约束，拓展现有的支持泛型约束机制的程序设计语言泛型约束的应用范围。 (2)在设计过程中，给出类型参数和操作参数两类泛型参数构成域的精确描述。 (3)提出PAR平台泛型约束匹配检测及验证模型及其相关算法，支持完善的模块化约束匹配自动检测，借助Isabelle定理证明器验证实例类型和实例操作与类型约束和操作约束的语义匹配关系。 (4)进一步设计泛型约束机制在PAR平台的实现方案及其系统原型，可将检验合法的泛型Apla程序自动生成可执行的C++程序，提高C++程序的泛型安全性。 1.3 本书的组织结构 本书共7章，各章的组织结构如下： 第1章为绪论部分，对撰写背景和研究内容进行概述。 第2章为综述部分，对国内外泛型程序设计和泛型约束的研究状况进行分析总结。 第3章概要介绍PAR方法和PAR平台，并重点阐述本书提出的泛型约束机制的宿主语言，即抽象程序设计语言Apla及其原有的泛型机制。 第4章提出泛型约束机制在Apla中的设计方案，包含数据类型约束和操作约束两类约束定义及其调用和例化方案。 第5章设计PAR平台泛型约束匹配检测及验证模型及其相关算法，支持完善的模块化约束匹配自动检测，借助Isabelle定理证明器验证实例类型和实例操作与类型约束和操作约束的语义匹配关系。 第6章设计泛型约束机制在PAR平台的实现方案及其系统原型，并将其成功应用于多个泛型实例，通过一个典型的基于闭半环代数结构约束的Kleene泛型算法展示该泛型约束机制的设计与实现过程。 第7章在对全书进行总结的基础上，讨论本书工作可能的后续扩展。 第2章 泛型约束相关研究 2.1 泛型程序设计 迄今为止，泛型程序设计的定义仍未统一[27]。Jarvi等认为泛型程序设计是设计和实现软件可重用部件库的一种范式，抽取算法相近实现的共性，并以尽可能参数化的方式覆盖这些实现，在力求抽象性的同时保持高效运行，*终得到抽象的泛型算法[28，29]。Hinze等认为泛型程序设计是函数式编程的一种范式，其中函数将类型作为参数，函数的行为取决于类型的结构[19，30]，这类函数称为泛型函数，编写一次泛型函数，可通过实例化不同的具体类型使用多次。Reis等认为泛型程序设计是软件设计的一种系统性方法，致力于抽取算法的*通用(或抽象)表示形式，并保持高效的运行方式[31-33]。Russo等给出了更广义的泛型程序设计的定义[34，35]：泛型程序设计是计算机科学的一个分支，主要是抽取算法、数据结构和其他软件概念的抽象表示，并将它们进行系统的组织。 根据现有的泛型程序设计的定义，本书认为典型的泛型程序设计是一个参数化程序设计(parameterized programming)，其中参数是指数据、数据类型、操作(函数和过程)、构件、服务和子系统等，并以此为基础，编制出具有通用性的程序。泛型程序设计的作用在于能编写清晰、易理解、可重用的程序，能反映程序中算法的实质，是编写抽象算法程序的有力工具。用泛型程序设计方法设计的程序称为泛型程序，泛型程序中的形参称为泛型参数，形参对应的实参称为实例参数。泛型程序设计以高效率和高抽象的特点已在产业界和学术界得到广泛关注和认可。 2.2 泛型程序设计及其约束的新定义 1997年起，Xue[21，22]一直致力于研究泛型程序设计，经过深入的研究，本书给出了更为确切的泛型程序设计及其约束的定义。 定义2-1(泛型程序设计)泛型程序设计是一个参数化程序设计，其中参数是指数据、数据类型、子程序(函数和过程)、构件、服务和子系统等，并以参数化程序设计为基础，编制出具有通用性的程序。 定义2-2(泛型约束)泛型约束是在泛型程序设计中对每类泛型参数构成域的精确描述。 例如，若泛型参数为数据，则其泛型约束即对数据域的精确描述，即类型，这是*低级的泛型约束；若泛型参数为数据类型，则其泛型约束即对数据类型的精确描述，依据任何一个标准数据类型都是一个代数系统的结论[36]，本书提出用代数结构来描述标准数据类型约束；若泛型参数为操作，则其泛型约束即对操作的精确描述，本书提出用Hoare公理语义来描述操作约束。泛型约束是保证泛型程序设计安全性的重要机制，也是构造可信软件的关键技术[37]。 从以上定义可以看出，完整的泛型约束应包含对数据、数据类型、操作(函数和过程)、构件、服务和子系统等每类泛型参数构成域的精确描述。然而，目前大多数语言只支持数据及数据类型的构成域的描述，并且对于数据类型约束也只涵盖了语法层的约束需求，对语义层约束也未涉及。 2.3 函数式语言泛型约束 将泛型程序设计引入现代函数式语言(如Haskell?98、ML等)中是当前研究的一大热点，其基本思想是在类型结构上归纳定义函数。 2.3.1 System F 泛型程序设计的思想源于20世纪60年代的函数式编程语言LISP，LISP提出高阶函数、参数化多态的编程方式；类型系统*终实现是在20世纪70年代，主要有两类： (1)Girard和Reynolds提出的System F； (2)Hindley-Milner类型系统。 System F[3，4]是由逻辑学家Jean-Yves Girard和计算机科学家John C. Reynolds分别独立设计的。System F提出了一种多态性的λ演算，构成了Haskell、ML等程序语言参数化多态的理论基础。System F的定义非常简明，其语法只支持两类特性，即函数和泛型，并且只支持一个参数。 System F的巴克斯-诺尔范式(Backus-Naur form，BNF)文法如下： System F的类型规则如下： 其中，代表e被定义为类型，且在范围内。在中是抽象，其形参变量是x，类型为，体部分是e，类型为。代表的输入参数类型为，输出参数类型为。在中，是泛型需求，代表任何符合泛型需求的类型。 2.3.2 Haskell 98 Haskell 98由低到高定义了三类层次结构[38]，即值(value)、类型(type)和类属(kind)，将结构强加于较低层次后可获得较高层次。定义参数化类型需要类属这一层次结构。 例2-1 用Haskell 98描述比较数据相等性的泛型模式举例。 记相等函数为EqT，其中下标T指定了函数EqT能够操作(运算)的数据类型，[T]为以T类型为基类型的序列类型。 此处的A为类属，所有可比较的具体类型(如int、char等)均可作为A的模型。 例2-2 用Haskell 98