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

基于函数式语义的循环和递归程序结构通用证明技术*李希萌1,2,王国辉1,3,张倩颖1,2,施智平1,2,关永1,31(首都师范大学信息工程学院,北京100048)2(电子系统可靠性技术北京市重点实验室(首都师范大学),北京100048)3(北京成像理论与技术高精尖创新中心(首都师范大学),北京100048)通信作者:施智平,E-mail:摘要:各类安全攸关系统的可靠运行离不开软件程序的正确执行.程序的演绎验证技术为程序执行的正确性提供高度保障.程序语言种类繁多,且用途覆盖高可靠性场景的新式语言不断涌现,难以为每种语言设计支撑其程序验证任务的整套逻辑规则,并证明其相对于形式语义的可靠性和完备性.语言无关的程序验证技术提供以程序语言的语义为参数的验证过程及其可靠性结果.对每种程序语言,提供其形式语义后可直接获得面向该语言的程序验证过程.提出一种面向大步操作语义的语言无关演绎验证技术,其核心是对不同语言中循环、递归等可导致无界行为的语法结构进行可靠推理的通用方法.特别地,借助大步操作语义的一种函数式形式化提供表达程序中子结构所执行计算的能力,从而允许借助辅助信息对子结构进行推理.证明所提出验证技术的可靠性和相对完备性,通过命令式、函数式语言中的程序验证实例初步评估了该技术的有效性,并在 Coq 辅助证明工具中形式化了所有理论结果和验证实例,为基于辅助证明工具实现面向大步语义的语言无关程序验证工具提供了基础.关键词:程序验证;大步操作语义;定理证明;Coq 定理证明器中图法分类号:TP311中文引用格式:李希萌,王国辉,张倩颖,施智平,关永.基于函数式语义的循环和递归程序结构通用证明技术.软件学报,2023,34(8):36863707.http:/ Proof Technique for Iterative and Recursive Program Structures Based on FunctionalSemanticsLIXi-Meng1,2,WANGGuo-Hui1,3,ZHANGQian-Ying1,2,SHIZhi-Ping1,2,GUANYong1,31(InformationEngineeringCollege,CapitalNormalUniversity,Beijing100048,China)2(BeijingKeyLaboratoryofElectronicSystemReliabilityTechnology(CapitalNormalUniversity),Beijing100048,China)3(BeijingAdvancedInnovationCenterforImagingTheoryandTechnology(CapitalNormalUniversity),Beijing100048,China)Abstract:Thereliablefunctioningofsafety-criticalITsystemsdependsheavilyonthecorrectexecutionofprograms.Deductiveprogramverificationcanbeperformedtoguaranteethecorrectexecutiontoalargeextent.Therearealreadyaplethoraofprogramminglanguagesin use,and new languages oriented toward high-reliability scenarios are still being invented.As a result,it is difficult to devise a full-fledgedlogicalsystemforeachlanguagetosupporttheverificationofprogramsandprovethesoundnessandcompletenessofthelogicalsystem with respect to the formal semantics of the language.Language-independent verification techniques offer sound verification*基金项目:国家重点研发计划(2019YFB1309900);国家自然科学基金(61876111,61877040,62002246);北京市教育委员会科技计划(KM201910028005,KM202010028010)本文由“形式化方法与应用”专题特约编辑陈立前副教授、孙猛教授推荐.收稿时间:2021-09-04;修改时间:2021-10-14,2022-01-10;采用时间:2022-01-27;jos 在线出版时间:2022-03-24CNKI 网络首发时间:2023-02-23软件学报ISSN1000-9825,CODENRUXUEWE-mail:Journal of Software,2023,34(8):36863707doi:10.13328/ki.jos.006616http:/中国科学院软件研究所版权所有.Tel:[phone]procedures parameterized over the formal semantics of programming languages.The specialization of the verification procedure with theformalsemanticsofaconcreteprogramminglanguagedirectlygivesrisetoaverificationprocedureforthelanguage.Thisstudyproposesa language-independent verification technique based on big-step operational semantics.The technique features a unified procedure forsound reasoning about program structures that potentially cause unbounded behavior,such as iteration and recursion.In particular,thestudy employs a functional formalization of big-step operational semantics to support the explicit representation of the computationperformedbythesub-structuresofaprogram.Thisrepresentationenablestheexploitationoftheauxiliaryinformationprovidedforthesesub-structuresintheunifiedreasoningprocess.Inaddition,thestudyhasprovedthesoundnessandrelativecompletenessoftheproposedtechnique,evaluated the technique by verification examples in imperative and functional programming languages,and formalized alltheoretical results and verification examples in the Coq proof assistant,and thus provides a basis for developing a language-independentprogramverifierwithbig-stepoperationalsemanticsbasedonaproofassistant.Key words:programverification;big-stepoperationalsemantics;theoremproving;Coqproofassistant软件程序的正确性是影响各类安全攸关系统可靠性的重要因素之一.为提供最高级别的正确性保障,往往使用形式化方法1对程序进行验证.在各类程序验证方法中,基于定理证明思想的演绎验证(deductiveverification)以程序语言的形式化语义为基础,对程序的正确性进行证明.当目标程序的正确性依据较为复杂,依赖于巧妙构思或深入领域知识时,演绎验证方法可为验证任务的完成提供有力帮助.若基于辅助证明工具(proofassistant)实现2程序的演绎验证,则能够给出高度可靠的验证结果.对程序进行演绎验证的基本方法是直接以某种操作语义3,4的规则作为公理或定理,构建程序正确性的数学证明.由于循环、函数调用等程序结构可能导致无界的程序行为(unboundedbehavior),往往须运用数学归纳法完成证明,其过程较为繁琐.一种简化思路是使用归纳不变式(inductiveinvariant)5,即构造逻辑表达式,使其被整个程序的初始条件蕴含,被程序的所有可能原子执行步骤保持,且蕴含所需保障的终止条件.此种方法原理简单清晰,然而构造能够刻画程序所有可达状态的不变式,则是一项复杂的工作.一类有效简化程序演绎验证的语义定义方式是公理语义3,4.它直接提供一系列逻辑规则,帮助推导关于各类语句执行结果的判断.然而,公理语义在反映程序语句含义方面的直观性不如操作语义,其正确性常借助与其他语义的等价性证明加以支撑.基于公理语义思想,发展出一系列程序逻辑,提供丰富策略以帮助对指针、函数调用、对象、并发等语言特性进行推理.许多强大的软件验证工具(如 Frama-C6、KeY7、Why38、VST9、Iris10等)支持基于程序逻辑对不同语言程序进行演绎验证.与公理语义情形类似,程序逻辑的正确性往往借助其相对某个基准语义(常为操作语义)的可靠性和完备性加以支撑.程序语言数量庞大,对于每种有验证需求的语言设计程序逻辑并完成可靠性和完备性证明是一项艰巨任务.语言无关(language-independent)的程序验证技术1114在一定程度上兼顾直接程序证明方法和程序逻辑的优势.此类技术的核心包括一个以操作语义为参数的验证过程和该过程的可靠性定理.对不同程序语言,在提供该语言的操作语义后可直接得到一个该语言程序的半自动验证过程.该过程基于用户给出的类似程序逻辑中循环、递归函数等关键结构的辅助信息,可靠验证程序的正确性.语言无关的程序验证技术解决的核心问题是如何对允许产生任意多执行步骤的程序结构(如循环、递归函数等),以一致的形式为其提供辅助信息,对其进行可靠推理.这是因为图灵完备的程序语言无论具有何种范式和特性,往往需要此类程序结构以支撑其表达能力.而此类结构的存在导致无法直接借助基于形式语义的符号执行完成程序的证明.当前支持以辅助证明工具为平台进行语言无关程序验证的技术11,12均依托于程序的小步操作语义15.与小步语义相比,大步语义16粒度较粗,较难用来描述并发执行.然而在许多情形下,大步语义的定义和使用相对简单,如在大步语义的语义格局中往往无需引入调用栈等控制结构,在使用大步语义的形式化证明中无需同时考虑推导序列(derivationsequence)和推导树(derivationtree)等.依托于大步语义的语言无关程序证明技术的研究,不仅可支撑未定义小步语义的程序语言中的验证任务,也有助于对一般程序语言,发挥大步语义本身能够简化某些证明任务的优势.本文提出一种能够基于大步操作语义进行程序验证的语言无关验证技术.语言无关的程序验证过程并不依赖于程序语言的语法结构,而是在语义层面利用程序中关键子结构执行相关的辅助信息,完整证明任务.小步语义描李希萌等:基于函数式语义的循环和递归程序结构通用证明技术3687c c述程序的单步执行(其中 c 和 c为语义格局),在此基础上,使用单步执行所构成的序列即可表征程序中子结构的执行.相较之下,大步语义提供描述程序完整执行的关系 ct(其中 c 为初始格局,t 为终止格局),若要获得其中子结构执行的表示,需要深入 ct 的推导过程进行检视.为解决这一问题,本文以特定的函数形式描述程序语言大步语义的语义规则,使得函数的一次应用对应于某个语义规则的一次使用,其复合应用则能表征大步语义推导树的一个子树,从而对程序中子结构的执行进行描述.此种函数式描述也使本文中理论结果和实例程序的证明往往能借助函数表达式的一系列化简加以实现.本文所提出技术包含以函数式大步操作语义为参数的验证过程及其可靠性定理.验证过程将目标语言中程序的验证转化为依托辅助信息的符号执行.所需辅助信息仅为关于程序中部分关键结构(如循环、递归函数)的局部信息,其作用类似于各种程序逻辑所需要的循环不变式和函数契约.本文给出该技术的可靠性证明,即若程序得到验证,那么程序满足部分正确性性质(partialcorrectness)17.本文通过命令式语言 While3中阶乘计算程序的演绎证明、非确定性卫式命令语言 GCarr(guardedcommandlanguage)18中数组极大值查找程序的演绎证明、函数式语言 Funlst中有序列表合并程序的演绎证明对所提出技术的有效性进行了初步评估.当辅助信息不足时(如缺少关键循环的不变式信息),可能出现形式规约中正确性性质得到满足,但无法得到证明的情形.本文证明若表征大步语义的函数为某种意义上的连续函数(见第 7 节),则能够向形式规约中添加辅助信息,以完成正确性证明,即在一定意义上,本技术亦具有完备性.本文所有理论结果和程序验证实例均在 Coq 辅助证明工具19中进行了形式化,除去所使用定理库的代码以及注释和空行,该形式化在 Coq 中的代码量约 3000 行.该形式化代码可在地址 https:/ 处获得.本文主要贡献可归结为如下 4 个内容.一个以程序语言的函数式大步语义为参数的可靠的程序验证过程.验证过程可靠性和相对完备性的证明.使用验证技术对不同范式程序语言的简单程序实例进行验证的过程和结果.所有理论结果和程序验证实例在 Coq 辅助证明工具中的形式化.本文第 1 节具体讨论主要相关工作.第 2 节介绍预备知识和符号约定.第 3 节给出基于函数式大步操作语义的语言无关验证技术并证明其可靠性.第 4 节依托简单命令式语言 While,介绍证明技术的具体使用方法.第 5、6 节给出含数组的卫式命令语言 GCarr以及含列表的函数式语言 Funlst中的进一步实例.第 7 节给出验证技术的相对完备性结果及其证明.第 8 节讨论本文所提出技术的其他方面,包括其局限性.第 9 节总结全文.1 主要相关工作 1.1 语言无关程序验证技术Moore 提出一种对程序进行演绎验证的技术11,可根据程序关键点处标注的断言生成归纳不变式(inductiveinvariant),如能验证该归纳不变式被程序的任何原子操作所保持,则程序得到验证.实质上该技术将类似于循环不变式的归纳断言(inductiveassertion)转化为归纳不变式,从而支持较少辅助信息下的可靠程序验证.该技术无需对每种程序语言单独证明此种转化的可靠性,故可视为一种语言无关的演绎验证技术.该技术针对程序的小步执行模型提出,建立在表达单步执行的二元关系的基础上.与之相比较,本文所提出技术适用于程序的大步操作语义,在原理上并不基于向归纳不变式的转化.Moore 等人提出一种在形式规约中辅助信息帮助下通过符号执行对程序进行可靠验证的技术12.该技术提供的验证过程以程序语言的小步操作语义为参数,其可靠性建立在最大不动点和余归纳法(coinduction)基础上.与之相比较,本文所提出技术适用于程序的大步操作语义,其可靠性建立在归纳推理基础上,较为直观.需要指出,本文所提出技术在形式规约的方式、相对完备性结果的形式方面从该工作中受到了启发.先于文献 12 的工作,同一研究组的 Stefanescu 等人提出一种基于重写系统和可达性逻辑(reachabilitylogic)的语言无关程序证明技术,在 KFramework 中进行了实现13.由于特定逻辑系统的支撑,该技术支持多种类型的3688软件学报2023 年第 34 卷第 8 期程序语义,包括小步、大步操作语义.相较之下,本文工作适用的语义类型较为单一.但另一方面,本文所提出技术只需辅助证明工具所提供的逻辑系统(如高阶逻辑)作为支撑,且无需程序语义以重写规则形式进行定义.由于本文所提出技术基于程序的大步而非小步执行模型,故较难用来处理程序语言中的并发特性.而另一方面,大步执行模型的定义及其在证明中的使用往往相对简单,如在大步操作语义中,一般无需通过引入额外程序语句对控制流状态进行记录;在其使用中,亦无需同时关注推导树和规约序列.大步语义同样具有广泛用途.1.2 基于翻译或转化的程序验证方法通过将被验证程序由某种形式语言进行表示,进而使用该形式语言的验证技术和工具对对象程序进行验证,亦可得到适用于多种不同语言的验证工具.此处形式语言可以为某种演算,如-演算、-演算等,可以为某种函数式程序语言,亦可以为某种命令式语言(如 LLVMIR 等中间语言).体现此种思想的工作包括但不限于文献 8,10,2022.基于翻译或转化的验证方法具有较强的实用性.其问题主要在于,使用形式语言对对象程序进行的表示(或者源语言向目标形式语言的翻译)是否恰当反映对象程序的实际语义,有时无法简单确认.对于某个语言翻译过程,若要充分确认其可靠性,最为稳妥的方法则是基于源语言和目标语言的形式化语义,证明待验证程序及其翻译结果的等价性.基于翻译或转化的程序验证技术与本文所提出技术具有不同原理和特点.1.3 程序逻辑程序逻辑相关研究工作是程序演绎验证方面的重要工作,既有研究成果众多,在本文范围内无法进行详细讨论.基本的霍尔逻辑17支持顺序程序的正确性证明;分离逻辑23提供支持局部推理的语法和规则,能够简化指针、并发等特性的演绎验证;假设-担保推理24适用于并发程序的组合式验证;动态逻辑25提供能够区分“存在某个执行”,或“全部执行”满足目标条件的算子;关系型程序逻辑(relationalprogramlogics)26支持对相互关联的多个程序执行的推理等.许多程序逻辑往往又存在为处理概率系统、实时系统、混成系统、量子程序等所进行的扩展.与本文所提出技术相比较,程序逻辑对于某种特定的程序语言提供更加全面的演绎验证支持,往往提供简化该语言所有特性相关推理的手段和规则.本文所提出技术和其他语言无关程序验证技术则侧重对循环、递归等可导致无界行为的语言特性推理的简化,但可同时适用于多种不同语言.2 预备知识 2.1 大步操作语义程序语言的大步操作语义(或大步语义)描述各类语法结构如何执行操作,将初始状态转化为终止状态.典型的初始状态包括程序的控制结构(控制状态)和各个变量的初始值(变量状态).控制状态和变量状态的组合通常称为语义格局(configuration).表示初始状态的语义格局称为初始格局(initialconfiguration).典型的终止状态给出各个变量的终值.考虑命名的一致性,下文将终止状态称为终止格局(terminalconfiguration).大步操作语义可借助一系列语义规则进行纸笔定义.下面以 While 语言3为例进行简单介绍.While 语言是一种高度简化的命令式语言.其语法结构包括算术表达式 a、布尔表达式 b、语句 S.语句 S 可以为执行空操作的语句 skip、赋值语句 x:=a、分支语句 ifb thenS1elseS2、循环语句 whilebdoS、顺序组合语句 S1;S2.设所有语句的集合为 Stmt.ABx 7 AAWhile 语言的大步语义规则如图 1 所示.其中 表示变量状态,是变量到整数的函数,a 表示算术表达式 a 在变量状态 下的求值结果,b 表示布尔表达式 b 在变量状态 下的求值结果,a 表示将变量 x 映射到值 a,并将其他变量 x映射到值 x的变量状态.该语义的初始格局为 Stmt 中元素,终止格局为 中元素.使用语义规则推导从某个初始格局(S,)出发能够到达的终止格局,需要构建以(S,)为根的有限高度的推导树(derivationtree),其所有叶子结点对应于无前提条件的规则(如 skip、赋值的规则或 While 循环条件为假的规则).关于简单顺序语句 x:=2;x:=10 执行结果的推导树如下所示:李希萌等:基于函数式语义的循环和递归程序结构通用证明技术3689(x:=2,)x 7 2(x:=10,x 7 2)x 7 2,x7 10(x:=2;x:=10,)x 7 2,x7 10.大步操作语义所描述的初始格局与终止格局间的二元关系实为使用语义规则所能推出的最小的初始格局、终止格局对的集合,理论上可通过最小不动点进行刻画.然而进行大步操作语义相关的理论证明或者使用大步操作语义进行程序证明时,往往使用推导树形状上的归纳法3,而无需考虑不动点概念.形式语义的定义工作以及基于形式语义的程序证明工作往往较为繁琐,容易出错.辅助证明工具(proofassistant)2提供有效的数理逻辑语言和手段,帮助进行精确无歧义的语义定义,并检查程序证明的所有步骤均符合数理逻辑的基本原则.在辅助证明工具中,常以归纳谓词27、求值函数28,29等方式对大步操作语义进行形式化,其形式化定义往往无法完全复刻图 1 中的纸笔定义,但反映相同的实质内容.(skip,)(x:=a,)x a 若 b =tt 若 b =ff 若 b =tt(while b do S,)若 b =ff(S1,)(S1;S2,)(S2,)(if b then S1 else S2,)(S,)(while b do S,)(while b do S,)(S1,)(S2,)(if b then S1 else S2,)图1While 语言大步操作语义的语义规则(纸笔定义形式)2.2 本文数学记号Pz Zzs Z本文使用记号 f a 表示数学函数 f 在参数 a 上的应用.有时为显式表示函数 f 的自变量 x,使用记号 x.f x 对函数 f 进行表示.函数应用操作具有左结合性,故 f a b 表示(f a)b,即函数 f 应用在参数 a 上,结果为另一函数 g,进而将该函数 g 应用在参数 b 上.对集合 A,使用(A)表示 A 的幂集,即 A 的所有子集构成的集合.本文所讨论的程序语言对整数和整数列表进行操作.用 表示空列表,用 z:zs 表示列表 zs 前附加整数 z 后所得的列表,用|zs|表示列表 zs 的长度,用 zsz1z2 表示这样的列表 zs,其第 z1个元素(z10,|zs|1)为 z2,而 zs的长度以及 zs中其他位置的元素均与列表 zs 相同.作为本文所使用元语言(metalanguage)的一部分,表达式 ifbthenPelseQ 在条件 b 成立时表示 P,否则表示 Q.不难根据上下文将其与对象语言中的类似表达式进行区分.3 程序证明技术及其可靠性 3.1 程序的形式规约设 C 为所有初始格局的集合,T 为所有终止格局的集合.P设 D:=C(T).即 D 中函数将每一个初始格局映射为一组可能的终止格局.对 D 中元素定义二元关系,使得 d1d2当且仅当对任意 c,有 d1c d2c.用表示 D 中的最小元素.故对任何初始格局 c,有c=.D 中的函数既可表示程序从具体初始格局所表达状态开始执行的结果,又可表示关于程序的形式规约.(1)当 D 中函数表示程序从具体初始格局所表达状态开始执行的结果时,该函数将每个初始格局 c 映射为由c 开始执行程序所能到达的终止格局集合.故无论对确定性语言还是对非确定性语言,D 中函数均能用来描述该语言程序的执行结果.(2)当 D 中函数用作程序的形式规约 时,该规约起到两个作用.首先,给出整个程序的正确性需求程序从每个 C 中格局 c 开始的实际执行结果应存在于集合 c 中.若 c=T,则表示对程序从初始格局 c 开始的执行结果不作限制.其次,给出关于程序中关键结构(如循环、递归函数等)执行结果的辅助信息对于某个语句和相应的初始格局 c,c 为该语句实际终止格局集合的超集.若 c=T,则表示对该语句未提供任何辅助信息,因为 T 包含形式系统中所有的终止格局.3690软件学报2023 年第 34 卷第 8 期以下给出用 D 中函数表达程序规约的一个示例.考虑如下的 While 语言程序 Sfac.fac:=m;while10fac(Swh,):=|(fac)=(fac)*(m 1)!若 m0fac c:=若初始格局 c 不满足以上条件形式规约 facD 所表达的正确性条件为:若从状态 开始执行语句 Sfac,且状态 下变量 m 为正数,那么执行终止后的状态 满足“(fac)=(m)!”.这表达了 Sfac终止后,变量 fac 的值应为 m 初值的阶乘,而除去 fac、m以外其他变量的值不予关心.形式规约 fac关于初始格局(Swh,)的部分具有如下含义.若某次到达循环头部时状态为,其中变量 m 为正数,则整个循环结束后,变量 fac 的值为“(fac)*(m1)!”.该部分的作用相当于程序逻辑中的循环不变式.若格局 c 不具备(Sfac,)或(Swh,)的形式,或其状态中变量 m 不为正数,则 fac c=,表示不关注由此种初始格局 c 开始执行的结果,或不需要提供关于此种初始格局 c 的辅助性信息.上述形式规约中,在条件 m0 下所指定的终止格局集合|(fac)=(m)!对应于程序逻辑中的霍尔三元组m=nn0Sfacfac=n!,其中 n 为逻辑变量(logicalvariable),用于记录程序变量 m 的初始值.形式规约 fac中允许使用程序状态,相应省去了该逻辑变量.对于不同的程序语言,霍尔三元组使用的断言语言(assertionlanguage)及其语义往往需要单独定义,好处是可以去掉对程序状态的显式引用,使形式规约更为简洁.相较之下,本文中形式规约 的定义对不同语言具有一致的形式,同时并未过度牺牲表达方面的简练程度(见第5.2、6.2 节实例).此外,对于具体的语言或语言特性,可考虑引入进一步记号以简化形式规约 的表达.若使用大步操作语义直接证明规约 fac得到满足,即 fac 的终值等于 m 初值的阶乘,需要使用基于推导树形状的归纳法(inductionontheshapeofderivationtrees)3证明 Sfac中循环结构的不变式.一般地,对于每个执行次数没有常数上界的循环,均需要对其不变式进行归纳证明.若改为使用霍尔逻辑进行阶乘程序的证明,则无需显式使用归纳法.但 While 语言的霍尔逻辑仅适用于 While 语言程序的正确性证明,对于每种新的程序语言,则需要为该语言设计专门的程序逻辑,并证明其关于操作语义的可靠性和完备性,其证明工作量往往随语言特性繁杂程度的增长而迅速增加.本节剩余部分所提出技术则允许基于任一程序语言大步操作语义的形式化定义,直接获得该语言程序的简单验证过程使用该验证过程无需关于待证程序中循环结构、递归函数的无界行为进行归纳推理.3.2 函数式大步语义形式化和程序正确性条件某种程序语言大步操作语义的纸笔定义通常由一系列如下形式的语义规则构成.c1 tn.c t若 c(1)直观上,该规则表示在借助逻辑谓词 表达的条件 c 下,若从每个初始格局 ci开始的执行结束时所能到达的终止格局包括 ti,且 c1cn、t1tn满足一定条件(未在规则中显示),那么从初始格局 c 开始的执行结束时所能到达的终止格局包括 t(t 与其他参数的联系未在规则中显示).P现考虑通过函数定义对大步语义进行形式化.具体引入一个函数 hDD(注意 D=C(T),由一系列如下形式的定义式给出:h f c:=t|t1 f c1tn f cn若 c.若函数 fD 能够对任一初始格局给出通过构造最大高度为 m 的推导树(derivationtree)所能导出的终止格局集合,那么 h f c 便给出使用语义规则(1)和关于 c1cn的子树构造高度为 m+1 的推导树所能导出的终止格局集合.若以此种定义式形式化大步语义的所有语义规则,则对于这样定义的 h,其在上的 k 次迭代结果(亦为 D李希萌等:基于函数式语义的循环和递归程序结构通用证明技术3691中的函数)即能对每个初始格局,给出通过构造最大高度为 k+1 的推导树,所能导出的相应终止格局集合.Var ZAB以下给出使用函数 h 对 While 语言的大步操作语义进行形式化的示例.具体化初始格局集合 C:=Stmt、终止格局集合 T:=,其中:=为变量状态集合.在此基础上,使用图 2 中函数 h 的定义形式化图 1 中 While语言的大步操作语义规则.图 2 中,和分别为算术表达式和布尔表达式的求值函数3.h f(skip,):=h f(x:=a,):=x a h f (if b then S1 else S2,):=f(S1,)(若 b =tt)h f (if b then S1 else S2,):=f(S2,)(若 b =ff)(若 b =tt)h f (while b do S,):=(若 b =ff)h f(S1;S2,):=|:f(S1,)f(S2,)h f(while b do S,):=|:f(S,)f(while b do S,)图2形式化 While 语言大步语义的函数 h图 2 中定义式 h f(ifbthenS1elseS2,):=f(S1,)形式化图 1 中 if 语句的第 1 条语义规则,表示分支条件为真时,若使用某个高度的操作语义推导树可导出(S1,)对应的终止格局集合 f(S1,),那么使用该规则构造高度增1 的语义推导树,可导出(ifbthenS1elseS2,)对应的终止格局集合 h f(ifbthenS1else S2,),它与(S1,)对应的终止格局集合相同.其他定义式如何对图 1 中的语义规则进行形式化,可类似解释.下面基于用函数 h 形式化的大步语义以及形式规约 给出程序的正确性条件.定义 1.正确性条件.若有n:hn,则称形式规约 得到满足,记作.本定义中,实际要求n c:hncc,即对任意初始格局,迭代函数 h 任意多次可得到的执行结果均在形式规约所规定的范围内.直观上,可解释为使用大步语义规则构造任何有限深度的推导树,所得到的从初始格局开始的执行结果均在形式规约所规定的范围内亦即程序的任何终止执行,其结果均在形式规约所规定的范围内.这是在不假设具体程序语言的情况下,对部分正确性条件(partialcorrectness)17的一般性表达.程序的正确性规约往往只关注执行结果所需满足的部分关键条件,故 c 中允许包含程序实际执行结果以外的元素.阶乘计算程序的形式规约即是一个具体例子.因此,定义 1 中使用“”而非“=”来表达程序执行结果和形式规约的关系.虽然本节仅给出使用函数 h 形式化 While 语言大步操作语义的示例,该方法同样适用于其他确定性、非确定语言.使用函数 h 形式化程序语言大步操作语义的其他示例在本文第 5、6 节中给出.3.3 程序正确性的验证定义函数 FDDD,使得:Ff:=h(f)f:=c.(ifc=Tthen f celsec)直观上,当形式规约 未能给出关于从初始格局 c 开始执行目标程序所得结果的任何信息时(即 c=T 时),F 通过函数 f 计算执行结果的范围,否则 F 通过形式规约 给出执行结果的可能范围.直观上,函数 F 借助形式规约 给出关于程序执行结果的近似范围.借助简单推导可证,对将任何初始格局均映射为 T 的形式规约 T,有 FT=h.这反映出当形式规约未提供任何有用信息时,F 退化为表达具体执行的函数 h.以下基于函数 F 给出程序的验证条件,亦即使用本文所提出技术直接证明的目标.定义 2.证明目标.若有n:(F)n,则称形式规约 得到验证,记作.在本定义中,实际要求n c:(F)ncc,即对任意初始格局,迭代函数(F)给出目标程序产生结果的可能范围均包在形式规约所要求的范围之内.定义中包含关于迭代次数 n 的全称量词,看似会使证明过程复杂化.但后文中程序证明实例显示,在形式规约 包含循环、递归等程序结构所需关键辅助信息的前提下,若要完成证明,只需假设一般 n 值,对(F)nc 进行化简(化简过程中可消去 n),并确认最终化简结果在 c 中.为保证验证的可靠性,以下证明 到 的逻辑蕴含.该证明无需假设 h 定义式的具体形式,但需要 h 单调.3692软件学报2023 年第 34 卷第 8 期定义 3.单调函数.若函数 fDD 满足对任何 d1d2,f d1f d2成立,则称 f 为单调函数.直观上不难看出,若函数 h 以第 3.2 节中方式对大步语义的规则进行形式化,则 h 为单调函数.一般地,可考虑严格刻画 h 定义式所具有的形式,从而证明一类函数 h 均为单调函数.但由于该形式的表达较繁,本文并不对其进行刻画.在第 46 节中,具体 h 定义的单调性均可通过简单机械的步骤加以证明.以下证明一关键引理.引理 1.假设 h 为单调函数.若 成立,则有n:hn(F)n.证明:在 n 上使用数学归纳法.若 n=0,有 hn=,以及(F)n=,故有 hn(F)n.若 n=k+1,其中 k0,则进行如下推导.(F)n=(F)(F)k)(由 n 次迭代函数的定义)=F(F)k)(由函数应用的左结合性)=h(F)k)(由 F 的定义)=hc.(ifc=Tthen(F)k)celsec)(由的定义)hc.(F)k)c)(说明(F)k)cc,h 单调)h c.(hk)c)(由归纳假设、h 的单调性)=hn证毕.上述引理指出若形式规约 能够得到验证,那么对任何 n 值,hn不超过(F)n,直观上表达具体计算结果可由基于 导出的抽象计算结果进行近似.基于引理 1 可直接导出下列可靠性定理.定理 1.验证技术的可靠性.假设 h 为单调函数.对任一形式规约,若有,则有.基于由单调函数 hDD 进行形式化的任何程序语言的大步语义,以上定理说明若能够证明(F)n对任一自然数 n 成立,则能够保证形式规约 的正确性.由于定理 1 的证明不依赖于某个具体的 h 定义(表征某个特定程序语言的语义),其所支撑的程序证明技术可视为一种语言无关11,12程序证明技术.第 4 节中的实例显示,本定理的使用能够省去基于大步语义的直接正确性证明中为处理每个目标程序中的循环、递归调用所需使用的归纳推理.4 While 语言程序证明示例本节使用定理 1 证明第 3.1 节中给出的 While 语言阶乘程序的形式规约得到满足,并讨论本文技术对循环结构的处理方式与霍尔式程序逻辑的差异.4.1 阶乘程序正确性证明关于第 3.2 节中 While 语言大步语义的形式化,容易证明下列引理.引理 2.图 2 中定义的函数 h 为单调函数.本引理的证明转化为对任意满足 f1f2的 f1、f2,和任意 c,证明 h f1ch f2c.对 c 中的语句进行分类讨论即可完成证明.在本引理基础上,即可使用第 3 节中定理 1 对任何 While 语言程序进行可靠验证.以下讨论第 3.1 节中形式规约 fac的证明.该证明的最终目标是说明 fac得到满足,即建立fac(见定义 1).使用定理 1,往证fac.即证明对每种可能的初始格局 c,有n:(Ffac)ncfacc.以下对 c 进行分类讨论.(1)若 c 不具有形式(Sfac,)或(Swh,),或者根据 c 中的状态,m 的值非正,则 facc=.此时显然有(Ffac)ncfacc,因为任何状态的集合