基于函数式语义的循环和递归程序结构通用证明技术

Unified Proof Technique for Iterative and Recursive Program Structures Based on Functional Semantics

各类安全攸关系统的可靠运行离不开软件程序的正确执行.程序的演绎验证技术为程序执行的正确性提供高度保障.程序语言种类繁多,且用途覆盖高可靠性场景的新式语言不断涌现,难以为每种语言设计支撑其程序验证任务的整套逻辑规则,并证明其相对于形式语义的可靠性和完备性.语言无关的程序验证技术提供以程序语言的语义为参数的验证过程及其可靠性结果.对每种程序语言,提供其形式语义后可直接获得面向该语言的程序验证过程.提出一种面向大步操作语义的语言无关演绎验证技术,其核心是对不同语言中循环、递归等可导致无界行为的语法结构进行可靠推理的通用方法.特别地,借助大步操作语义的一种函数式形式化提供表达程序中子结构所执行计算的能力,从而允许借助辅助信息对子结构进行推理.证明所提出验证技术的可靠性和相对完备性,通过命令式、函数式语言中的程序验证实例初步评估了该技术的有效性,并在Coq辅助证明工具中形式化了所有理论结果和验证实例,为基于辅助证明工具实现面向大步语义的语言无关程序验证工具提供了基础.

The reliable functioning of safety-critical IT systems depends heavily on the correct execution of programs.Deductive program verification can be performed to guarantee the correct execution to a large extent.There are already a plethora of programming languages in use,and new languages oriented toward high-reliability scenarios are still being invented.As a result,it is difficult to devise a full-fledged logical system for each language to support the verification of programs and prove the soundness and completeness of the logical system with respect to the formal semantics of the language.Language-independent verification techniques offer sound verification procedures parameterized over the formal semantics of programming languages.The specialization of the verification procedure with the formal semantics of a concrete programming language directly gives rise to a verification procedure for the language.This study proposes a language-independent verification technique based on big-step operational semantics.The technique features a unified procedure for sound reasoning about program structures that potentially cause unbounded behavior,such as iteration and recursion.In particular,the study employs a functional formalization of big-step operational semantics to support the explicit representation of the computation performed by the sub-structures of a program.This representation enables the exploitation of the auxiliary information provided for these sub-structures in the unified reasoning process.In addition,the study has proved the soundness and relative completeness of the proposed technique,evaluated the technique by verification examples in imperative and functional programming languages,and formalized all theoretical results and verification examples in the Coq proof assistant,and thus provides a basis for developing a language-independent program verifier with big-step operational semantics based on a proof assistant.