2722 Journal of Software软件学报ol.19,No.10.October2008 Code Proof (Foundational logic) Type system Recursive func. Proof checker soundness soundness Fig.2 FPCC built with recursive functions 图2使用递归函数构造的FPCC 因为递归函数不是独立于基础逻辑系统之外的，而是定义在基础逻辑系统之中，所以此证明构造方法具有 如下优势：()由于使用递归函数代替了部分或全部的推理规则，则证明构造过程可以（半）自动完成，从而提高 了证明构造的自动化程度，易于代码生产方产生FPCC代码.(2)利用递归函数构造的证明不会随着可执行代码 的长度增长而大幅度增长，证明检查过程中避免了操作规模庞大的证明(3)定义在基础逻辑系统之中的递归 函数不需要被信任，即不属于系统的TCB.代码消费方在检查安全性证明时，除了基础逻辑证明检查器之外，不 再需要信任额外的检查程序(4)代码携带的安全性证明仍然是严格意义上的基础的安全性证明，不局限于某 一种特定的推理系统，因此，证明可以基于多态类型系统、一阶算术逻辑系统、或者是多种由不同形式推理系 统构成的混合系统.（⑤）此方法可以与己有的证明构造方法(TALT,CAP等系统)相结合. 本文第2节使用一个简单的例子来解释此证明构造方法的步骤和原理第3节介绍此方法在一个简化的 FPCC系统中的应用.由于篇幅所限，本文只给出涉及文中内容部分的形式定义与相关定理证明的大概思路.该 FPCC系统的全部内容都己在证明辅助工具Coq中实现，完整的实现代码可以从本文的网站 (http:∥ssg.ustcsZ.edu.cn/~guoyu/proof功上下载.该方法已被应用到了垃圾收集器2]与多线程库l]的证明中第4 节简要介绍C0q代码实现与实验结论.第5节比较相关的工作，最后一节为结束语. 2利用辅助递归函数构造证明 假设一个定理的证明基于一些推理规则（定义在基础逻辑系统内部），如果由这些推理规则构成的证明可以 找到一种算法来机械地完成构造，那么可以（在基础逻辑系统内部）定义递归函数实现这一算法，然后代替原有 的推理规则来构造证明此外，递归函数关于推理规则的可靠性必须在基础逻辑系统内部被证明利用此递归函 数与其可靠性证明，我们就可以构造与原来使用推理规则构造的证明等价的证明.下面将通过一个简单的例子 来解释如何利用辅助递归函数构造证明」 2.1基于推理系统的证明构造 下面定义一个推理系统来推理一个自然数是否是斐波纳奇(Fibonacci)数： 0b1 (fibz) 1 (fibo) mPnm+lP凸(6bp) mon (fib) m+2D2,+几， Fibn 其中，m>n表示斐波纳奇数列的第m个数是n,Fbn表示n属于斐波纳奇数列.推理规则在CiC中定义为 Fib fibz:0 1 fibo:11 1fbp:(mDn)→(m+1>nz2)→(m+2)P(+n2) 1fib:(3m.mpn)→Fibn 其中，fibz,fibo,fibp与fib是Fib谓词的构造符(constructor),fibp与fib构造符是函数项.由上面推理规则可知， 命题Fb3与命题Fb8是此推理系统中的定理，其证明用项表示如下： (3,fibp fibo (fibp fibz fibo)):Fib 3 (5,(fibp fibo (fibp fibz fibo))(fibp (fibp fibz fibo)(fibp fibo (fibp fibz fibo)))):Fib 8 这里的符号(x,a)表示依赖对，即命题x.T的证明，其中a的类型是T.命题Fib34也是此推理系统的一个定理，但 此定理的证明项的规模接近1000字节.尽管这些证明项中都存在着一定冗余，但是经过优化之后其规模仍然 难以避免地随着输入数值的增加而大幅增长2722 Journal of Software 软件学报 Vol.19, No.10, October 2008 因为递归函数不是独立于基础逻辑系统之外的,而是定义在基础逻辑系统之中,所以此证明构造方法具有 如下优势:(1) 由于使用递归函数代替了部分或全部的推理规则,则证明构造过程可以(半)自动完成,从而提高 了证明构造的自动化程度,易于代码生产方产生 FPCC 代码.(2) 利用递归函数构造的证明不会随着可执行代码 的长度增长而大幅度增长,证明检查过程中避免了操作规模庞大的证明.(3) 定义在基础逻辑系统之中的递归 函数不需要被信任,即不属于系统的 TCB.代码消费方在检查安全性证明时,除了基础逻辑证明检查器之外,不 再需要信任额外的检查程序.(4) 代码携带的安全性证明仍然是严格意义上的基础的安全性证明,不局限于某 一种特定的推理系统,因此,证明可以基于多态类型系统、一阶算术逻辑系统、或者是多种由不同形式推理系 统构成的混合系统.(5) 此方法可以与已有的证明构造方法(TALT,CAP 等系统)相结合. 本文第 2 节使用一个简单的例子来解释此证明构造方法的步骤和原理.第 3 节介绍此方法在一个简化的 FPCC 系统中的应用.由于篇幅所限,本文只给出涉及文中内容部分的形式定义与相关定理证明的大概思路.该 FPCC 系统的全部内容都已在证明辅助工具 Coq 中实现 , 完整的实现代码可以从本文的网站 (http://ssg.ustcsz.edu.cn/~guoyu/proof/)上下载.该方法已被应用到了垃圾收集器[12]与多线程库[13]的证明中.第 4 节简要介绍 Coq 代码实现与实验结论.第 5 节比较相关的工作.最后一节为结束语. 2 利用辅助递归函数构造证明 假设一个定理的证明基于一些推理规则(定义在基础逻辑系统内部),如果由这些推理规则构成的证明可以 找到一种算法来机械地完成构造,那么可以(在基础逻辑系统内部)定义递归函数实现这一算法,然后代替原有 的推理规则来构造证明.此外,递归函数关于推理规则的可靠性必须在基础逻辑系统内部被证明.利用此递归函 数与其可靠性证明,我们就可以构造与原来使用推理规则构造的证明等价的证明.下面将通过一个简单的例子 来解释如何利用辅助递归函数构造证明. 2.1 基于推理系统的证明构造 下面定义一个推理系统来推理一个自然数是否是斐波纳奇(Fibonacci)数: 1 2 1 2 1 (fibz) (fibo) (fibp) (fib) 0 1 1 1 2 Fib mn m n mn m nn n + + +     其中,m  n 表示斐波纳奇数列的第 m 个数是 n,Fib n 表示 n 属于斐波纳奇数列.推理规则在 CiC 中定义为 1 2 12 Fib fibz : 0 1| fibo :1 1 | fibp : ( ) ( 1 ) ( 2) ( ) | fib : ( . ) Fib mn m n m n n mm n n →+ →+ + ∃ →      其中,fibz,fibo,fibp 与 fib 是 Fib 谓词的构造符(constructor),fibp 与 fib 构造符是λ函数项.由上面推理规则可知, 命题 Fib 3 与命题 Fib 8 是此推理系统中的定理,其证明用λ项表示如下: 〈 〉 3,fibp fibo (fibp fibz fibo) : Fib 3 〈 〉 5,(fibp fibo (fibp fibz fibo)) (fibp (fibp fibz fibo) (fibp fibo (fibp fibz fibo))) : Fib 8 这里的符号〈x,a〉表示依赖对,即命题∃x.T 的证明,其中 a 的类型是 T.命题 Fib 34 也是此推理系统的一个定理,但 此定理的证明项的规模接近 1 000 字节.尽管这些证明项中都存在着一定冗余,但是经过优化之后其规模仍然 难以避免地随着输入数值的增加而大幅增长. Fig.2 FPCC built with recursive functions 图 2 使用递归函数构造的 FPCC Proof Recursive func. & soundness Code (Foundational logic) Proof checker Type system & soundness