×

一种自动生成循环摘要的方法

消耗积分:2 | 格式:rar | 大小:1.07 MB | 2017-12-29

分享资料个

  采用形式化方法证明软件的正确性,是保障软件可靠性的有效方法.而对循环语句的分析与验证,是形式化证明中的关键对循环语句的处理一直是程序分析与验证中的一个难点问题.提出使用循环语句修改的内存和这些内存中存放的新值来描述循环语句的执行效果,并将该执行效果定义为循环摘要,同时,提出一种自动生成循环摘要的方法,可以为操作常用数据结构的循环自动生成循环摘要,包含嵌套循环.此外,基于循环摘要,可以自动生成循环语句的规约。包括循环不变式、循环的前置条件以及循环的后置条件.已经实现了自动生成循环摘要以及循环规约的方法,并将它们集成到验证工具Accumulator中.实验结果表明,该方法可以有效地生成循环摘要,并生成多种类型的规约,从而辅助软件程序的形式化证明,提高验证的自动化程度和效率,减轻验证人员的负担.
 

声明:本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人,不代表电子发烧友网立场。文章及其配图仅供工程师学习之用,如有内容侵权或者其他违规问题,请联系本站处理。 举报投诉

评论(0)
发评论

下载排行榜

全部0条评论

快来发表一下你的评论吧 !