基于函数式语义的循环和递归程序结构通用证明技术.pdf
《基于函数式语义的循环和递归程序结构通用证明技术.pdf》由会员分享,可在线阅读,更多相关《基于函数式语义的循环和递归程序结构通用证明技术.pdf(22页珍藏版)》请在咨信网上搜索。
1、基于函数式语义的循环和递归程序结构通用证明技术*李希萌1,2,王国辉1,3,张倩颖1,2,施智平1,2,关永1,31(首都师范大学信息工程学院,北京100048)2(电子系统可靠性技术北京市重点实验室(首都师范大学),北京100048)3(北京成像理论与技术高精尖创新中心(首都师范大学),北京100048)通信作者:施智平,E-mail:摘要:各类安全攸关系统的可靠运行离不开软件程序的正确执行.程序的演绎验证技术为程序执行的正确性提供高度保障.程序语言种类繁多,且用途覆盖高可靠性场景的新式语言不断涌现,难以为每种语言设计支撑其程序验证任务的整套逻辑规则,并证明其相对于形式语义的可靠性和完备性.
2、语言无关的程序验证技术提供以程序语言的语义为参数的验证过程及其可靠性结果.对每种程序语言,提供其形式语义后可直接获得面向该语言的程序验证过程.提出一种面向大步操作语义的语言无关演绎验证技术,其核心是对不同语言中循环、递归等可导致无界行为的语法结构进行可靠推理的通用方法.特别地,借助大步操作语义的一种函数式形式化提供表达程序中子结构所执行计算的能力,从而允许借助辅助信息对子结构进行推理.证明所提出验证技术的可靠性和相对完备性,通过命令式、函数式语言中的程序验证实例初步评估了该技术的有效性,并在 Coq 辅助证明工具中形式化了所有理论结果和验证实例,为基于辅助证明工具实现面向大步语义的语言无关程序
3、验证工具提供了基础.关键词:程序验证;大步操作语义;定理证明;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(I
4、nformationEngineeringCollege,CapitalNormalUniversity,Beijing100048,China)2(BeijingKeyLaboratoryofElectronicSystemReliabilityTechnology(CapitalNormalUniversity),Beijing100048,China)3(BeijingAdvancedInnovationCenterforImagingTheoryandTechnology(CapitalNormalUniversity),Beijing100048,China)Abstract:The
5、reliablefunctioningofsafety-criticalITsystemsdependsheavilyonthecorrectexecutionofprograms.Deductiveprogramverificationcanbeperformedtoguaranteethecorrectexecutiontoalargeextent.Therearealreadyaplethoraofprogramminglanguagesin use,and new languages oriented toward high-reliability scenarios are stil
6、l 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 verif
7、ication*基金项目:国家重点研发计划(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
8、Software,2023,34(8):36863707doi:10.13328/ki.jos.006616http:/中国科学院软件研究所版权所有.Tel:+86-10-62562563procedures parameterized over the formal semantics of programming languages.The specialization of the verification procedure with theformalsemanticsofaconcreteprogramminglanguagedirectlygivesrisetoaverifica
9、tionprocedureforthelanguage.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 parti
10、cular,thestudy employs a functional formalization of big-step operational semantics to support the explicit representation of the computationperformedbythesub-structuresofaprogram.Thisrepresentationenablestheexploitationoftheauxiliaryinformationprovidedforthesesub-structuresintheunifiedreasoningproc
11、ess.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
12、 basis for developing a language-independentprogramverifierwithbig-stepoperationalsemanticsbasedonaproofassistant.Key words:programverification;big-stepoperationalsemantics;theoremproving;Coqproofassistant软件程序的正确性是影响各类安全攸关系统可靠性的重要因素之一.为提供最高级别的正确性保障,往往使用形式化方法1对程序进行验证.在各类程序验证方法中,基于定理证明思想的演绎验证(deductiv
13、everification)以程序语言的形式化语义为基础,对程序的正确性进行证明.当目标程序的正确性依据较为复杂,依赖于巧妙构思或深入领域知识时,演绎验证方法可为验证任务的完成提供有力帮助.若基于辅助证明工具(proofassistant)实现2程序的演绎验证,则能够给出高度可靠的验证结果.对程序进行演绎验证的基本方法是直接以某种操作语义3,4的规则作为公理或定理,构建程序正确性的数学证明.由于循环、函数调用等程序结构可能导致无界的程序行为(unboundedbehavior),往往须运用数学归纳法完成证明,其过程较为繁琐.一种简化思路是使用归纳不变式(inductiveinvariant)5
14、,即构造逻辑表达式,使其被整个程序的初始条件蕴含,被程序的所有可能原子执行步骤保持,且蕴含所需保障的终止条件.此种方法原理简单清晰,然而构造能够刻画程序所有可达状态的不变式,则是一项复杂的工作.一类有效简化程序演绎验证的语义定义方式是公理语义3,4.它直接提供一系列逻辑规则,帮助推导关于各类语句执行结果的判断.然而,公理语义在反映程序语句含义方面的直观性不如操作语义,其正确性常借助与其他语义的等价性证明加以支撑.基于公理语义思想,发展出一系列程序逻辑,提供丰富策略以帮助对指针、函数调用、对象、并发等语言特性进行推理.许多强大的软件验证工具(如 Frama-C6、KeY7、Why38、VST9、
15、Iris10等)支持基于程序逻辑对不同语言程序进行演绎验证.与公理语义情形类似,程序逻辑的正确性往往借助其相对某个基准语义(常为操作语义)的可靠性和完备性加以支撑.程序语言数量庞大,对于每种有验证需求的语言设计程序逻辑并完成可靠性和完备性证明是一项艰巨任务.语言无关(language-independent)的程序验证技术1114在一定程度上兼顾直接程序证明方法和程序逻辑的优势.此类技术的核心包括一个以操作语义为参数的验证过程和该过程的可靠性定理.对不同程序语言,在提供该语言的操作语义后可直接得到一个该语言程序的半自动验证过程.该过程基于用户给出的类似程序逻辑中循环、递归函数等关键结构的辅助信
16、息,可靠验证程序的正确性.语言无关的程序验证技术解决的核心问题是如何对允许产生任意多执行步骤的程序结构(如循环、递归函数等),以一致的形式为其提供辅助信息,对其进行可靠推理.这是因为图灵完备的程序语言无论具有何种范式和特性,往往需要此类程序结构以支撑其表达能力.而此类结构的存在导致无法直接借助基于形式语义的符号执行完成程序的证明.当前支持以辅助证明工具为平台进行语言无关程序验证的技术11,12均依托于程序的小步操作语义15.与小步语义相比,大步语义16粒度较粗,较难用来描述并发执行.然而在许多情形下,大步语义的定义和使用相对简单,如在大步语义的语义格局中往往无需引入调用栈等控制结构,在使用大步
17、语义的形式化证明中无需同时考虑推导序列(derivationsequence)和推导树(derivationtree)等.依托于大步语义的语言无关程序证明技术的研究,不仅可支撑未定义小步语义的程序语言中的验证任务,也有助于对一般程序语言,发挥大步语义本身能够简化某些证明任务的优势.本文提出一种能够基于大步操作语义进行程序验证的语言无关验证技术.语言无关的程序验证过程并不依赖于程序语言的语法结构,而是在语义层面利用程序中关键子结构执行相关的辅助信息,完整证明任务.小步语义描李希萌等:基于函数式语义的循环和递归程序结构通用证明技术3687c c述程序的单步执行(其中 c 和 c为语义格局),在此基
18、础上,使用单步执行所构成的序列即可表征程序中子结构的执行.相较之下,大步语义提供描述程序完整执行的关系 ct(其中 c 为初始格局,t 为终止格局),若要获得其中子结构执行的表示,需要深入 ct 的推导过程进行检视.为解决这一问题,本文以特定的函数形式描述程序语言大步语义的语义规则,使得函数的一次应用对应于某个语义规则的一次使用,其复合应用则能表征大步语义推导树的一个子树,从而对程序中子结构的执行进行描述.此种函数式描述也使本文中理论结果和实例程序的证明往往能借助函数表达式的一系列化简加以实现.本文所提出技术包含以函数式大步操作语义为参数的验证过程及其可靠性定理.验证过程将目标语言中程序的验证
19、转化为依托辅助信息的符号执行.所需辅助信息仅为关于程序中部分关键结构(如循环、递归函数)的局部信息,其作用类似于各种程序逻辑所需要的循环不变式和函数契约.本文给出该技术的可靠性证明,即若程序得到验证,那么程序满足部分正确性性质(partialcorrectness)17.本文通过命令式语言 While3中阶乘计算程序的演绎证明、非确定性卫式命令语言 GCarr(guardedcommandlanguage)18中数组极大值查找程序的演绎证明、函数式语言 Funlst中有序列表合并程序的演绎证明对所提出技术的有效性进行了初步评估.当辅助信息不足时(如缺少关键循环的不变式信息),可能出现形式规约中
20、正确性性质得到满足,但无法得到证明的情形.本文证明若表征大步语义的函数为某种意义上的连续函数(见第 7 节),则能够向形式规约中添加辅助信息,以完成正确性证明,即在一定意义上,本技术亦具有完备性.本文所有理论结果和程序验证实例均在 Coq 辅助证明工具19中进行了形式化,除去所使用定理库的代码以及注释和空行,该形式化在 Coq 中的代码量约 3000 行.该形式化代码可在地址 https:/ 处获得.本文主要贡献可归结为如下 4 个内容.一个以程序语言的函数式大步语义为参数的可靠的程序验证过程.验证过程可靠性和相对完备性的证明.使用验证技术对不同范式程序语言的简单程序实例进行验证的过程和结果.
21、所有理论结果和程序验证实例在 Coq 辅助证明工具中的形式化.本文第 1 节具体讨论主要相关工作.第 2 节介绍预备知识和符号约定.第 3 节给出基于函数式大步操作语义的语言无关验证技术并证明其可靠性.第 4 节依托简单命令式语言 While,介绍证明技术的具体使用方法.第 5、6 节给出含数组的卫式命令语言 GCarr以及含列表的函数式语言 Funlst中的进一步实例.第 7 节给出验证技术的相对完备性结果及其证明.第 8 节讨论本文所提出技术的其他方面,包括其局限性.第 9 节总结全文.1 主要相关工作 1.1 语言无关程序验证技术Moore 提出一种对程序进行演绎验证的技术11,可根据程
22、序关键点处标注的断言生成归纳不变式(inductiveinvariant),如能验证该归纳不变式被程序的任何原子操作所保持,则程序得到验证.实质上该技术将类似于循环不变式的归纳断言(inductiveassertion)转化为归纳不变式,从而支持较少辅助信息下的可靠程序验证.该技术无需对每种程序语言单独证明此种转化的可靠性,故可视为一种语言无关的演绎验证技术.该技术针对程序的小步执行模型提出,建立在表达单步执行的二元关系的基础上.与之相比较,本文所提出技术适用于程序的大步操作语义,在原理上并不基于向归纳不变式的转化.Moore 等人提出一种在形式规约中辅助信息帮助下通过符号执行对程序进行可靠验
23、证的技术12.该技术提供的验证过程以程序语言的小步操作语义为参数,其可靠性建立在最大不动点和余归纳法(coinduction)基础上.与之相比较,本文所提出技术适用于程序的大步操作语义,其可靠性建立在归纳推理基础上,较为直观.需要指出,本文所提出技术在形式规约的方式、相对完备性结果的形式方面从该工作中受到了启发.先于文献 12 的工作,同一研究组的 Stefanescu 等人提出一种基于重写系统和可达性逻辑(reachabilitylogic)的语言无关程序证明技术,在 KFramework 中进行了实现13.由于特定逻辑系统的支撑,该技术支持多种类型的3688软件学报2023 年第 34 卷
24、第 8 期程序语义,包括小步、大步操作语义.相较之下,本文工作适用的语义类型较为单一.但另一方面,本文所提出技术只需辅助证明工具所提供的逻辑系统(如高阶逻辑)作为支撑,且无需程序语义以重写规则形式进行定义.由于本文所提出技术基于程序的大步而非小步执行模型,故较难用来处理程序语言中的并发特性.而另一方面,大步执行模型的定义及其在证明中的使用往往相对简单,如在大步操作语义中,一般无需通过引入额外程序语句对控制流状态进行记录;在其使用中,亦无需同时关注推导树和规约序列.大步语义同样具有广泛用途.1.2 基于翻译或转化的程序验证方法通过将被验证程序由某种形式语言进行表示,进而使用该形式语言的验证技术和
25、工具对对象程序进行验证,亦可得到适用于多种不同语言的验证工具.此处形式语言可以为某种演算,如-演算、-演算等,可以为某种函数式程序语言,亦可以为某种命令式语言(如 LLVMIR 等中间语言).体现此种思想的工作包括但不限于文献 8,10,2022.基于翻译或转化的验证方法具有较强的实用性.其问题主要在于,使用形式语言对对象程序进行的表示(或者源语言向目标形式语言的翻译)是否恰当反映对象程序的实际语义,有时无法简单确认.对于某个语言翻译过程,若要充分确认其可靠性,最为稳妥的方法则是基于源语言和目标语言的形式化语义,证明待验证程序及其翻译结果的等价性.基于翻译或转化的程序验证技术与本文所提出技术具
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 基于 函数 语义 循环 递归 程序结构 通用 证明 技术
1、咨信平台为文档C2C交易模式,即用户上传的文档直接被用户下载,收益归上传人(含作者)所有;本站仅是提供信息存储空间和展示预览,仅对用户上传内容的表现方式做保护处理,对上载内容不做任何修改或编辑。所展示的作品文档包括内容和图片全部来源于网络用户和作者上传投稿,我们不确定上传用户享有完全著作权,根据《信息网络传播权保护条例》,如果侵犯了您的版权、权益或隐私,请联系我们,核实后会尽快下架及时删除,并可随时和客服了解处理情况,尊重保护知识产权我们共同努力。
2、文档的总页数、文档格式和文档大小以系统显示为准(内容中显示的页数不一定正确),网站客服只以系统显示的页数、文件格式、文档大小作为仲裁依据,平台无法对文档的真实性、完整性、权威性、准确性、专业性及其观点立场做任何保证或承诺,下载前须认真查看,确认无误后再购买,务必慎重购买;若有违法违纪将进行移交司法处理,若涉侵权平台将进行基本处罚并下架。
3、本站所有内容均由用户上传,付费前请自行鉴别,如您付费,意味着您已接受本站规则且自行承担风险,本站不进行额外附加服务,虚拟产品一经售出概不退款(未进行购买下载可退充值款),文档一经付费(服务费)、不意味着购买了该文档的版权,仅供个人/单位学习、研究之用,不得用于商业用途,未经授权,严禁复制、发行、汇编、翻译或者网络传播等,侵权必究。
4、如你看到网页展示的文档有www.zixin.com.cn水印,是因预览和防盗链等技术需要对页面进行转换压缩成图而已,我们并不对上传的文档进行任何编辑或修改,文档下载后都不会有水印标识(原文档上传前个别存留的除外),下载后原文更清晰;试题试卷类文档,如果标题没有明确说明有答案则都视为没有答案,请知晓;PPT和DOC文档可被视为“模板”,允许上传人保留章节、目录结构的情况下删减部份的内容;PDF文档不管是原文档转换或图片扫描而得,本站不作要求视为允许,下载前自行私信或留言给上传者【自信****多点】。
5、本文档所展示的图片、画像、字体、音乐的版权可能需版权方额外授权,请谨慎使用;网站提供的党政主题相关内容(国旗、国徽、党徽--等)目的在于配合国家政策宣传,仅限个人学习分享使用,禁止用于任何广告和商用目的。
6、文档遇到问题,请及时私信或留言给本站上传会员【自信****多点】,需本站解决可联系【 微信客服】、【 QQ客服】,若有其他问题请点击或扫码反馈【 服务填表】;文档侵犯商业秘密、侵犯著作权、侵犯人身权等,请点击“【 版权申诉】”(推荐),意见反馈和侵权处理邮箱:1219186828@qq.com;也可以拔打客服电话:4008-655-100;投诉/维权电话:4009-655-100。