论文部分内容阅读
交互式定理证明技术是可以应用于大规模系统验证的重要的形式化方法，近年有一些影响很广的成功案例。但是交互式定理证明的使用难度以及对使用人员的严重依赖阻碍了其在工业界的发展。本文围绕主流的交互式定理证明工具之一的Coq，总结了其应用过程中的问题，分析了问题的原因，并在此基础上从其基础理论和应用实践两方面入手尝试提高Coq在实际应用过程中的易用性。在理论方面，针对Coq在使用中对依赖类型等价关系判定能力不足的问题，对Coq基础理论进行了扩展，并通过验证扩展后理论的主要性质，保证扩展的理论同样可以应用于实现定理证明工具。在应用实践方面，针对组合逻辑提出了基于Coq的验证框架。该框架提供了对组合逻辑建模验证的统一方法，也提供了面向组合逻辑验证的扩展库。对算术计算逻辑单元的实际验证工作说明了该框架的可用性和易用性。本文的主要工作包含以下几个方面：1.扩展了Coq的基础理论：归纳构造演算。在内涵式的归纳构造演算等价判定的基础上增加了外延式等价关系的判定能力，并且给出了扩展理论应用于实现定理证明工具的机制。外延式理论是抽象表示的，并被一些约束所限制，所有满足限制的外延式理论都可以被扩充进归纳构造演算的等价判定中。2.证明了扩展后的理论依然保持归纳构造演算的主要性质，从而保证了新的演算可以被应用于实现可靠的定理证明工具。由于语义方面性质的证明比较复杂，本文对语义方面性质的证明是在定理证明工具Coq中完成的，定理证明工具可以有效的管理证明并保证证明的正确性。3.通过证明Presburger代数满足限制的方式，为扩展的理论补充了外延式理论实例。Presburger代数可用于对Coq中常用的自然数类型的等价关系判定。4.提出了基于Coq的组合逻辑验证框架。框架提供了对组合逻辑建模验证的统一方法和面向组合逻辑的扩展库。使用框架对组合逻辑验证一方面可以减少前期调研的工作量，另一方面框架具有真实性、灵活性、模块化等特点可以简化组合逻辑验证工作并提高验证结论的适用性。5.通过对计算逻辑中加法器全面的验证，说明了框架的可用性和易用性。对加法器的全面验证结论可以作为扩展库的一部分为未来的验证提供基础。