摘要
提出了一种求解命令式程序中循环执行和终止条件的方法。该方法基于循环代码本身进行循环执行和终止条件的分析推导,可以定义一个原型工具进行自动化推导。现有的形式化方法依赖于形式化规范,而提出的方法适用于未被形式化的程序。提出的形式化方法可以在一个原型工具中实现,通过该工具来推导循环执行和终止条件,辅助程序验证和程序缺陷修正。
An approach to the analysis of loop progress and termination conditions is introduced in imperative programs. The approach involves the algorithmic derivation of loop progress and termination conditions directly from the code itself. The derivation of these conditions is automated in a prototype tool. Unlike existing formal approaches to termination investigation,which are reliant on the presence of formal specifications,this approach is applicable to undocumented programs as well as formally specified programs. It＇s presented the formal methods implemented in a prototype tool for deriving loop progress and termination conditions and use the output generated by the tool to illustrate its use in supporting verification and defect correction.
出处
《计算机工程与设计》
CSCD
北大核心
2010年第14期3193-3197,共5页
Computer Engineering and Design
关键词
循环执行
循环终止
形式化方法
自动化
程序验证
缺陷修正
loop progress
loop termination
formal method
automated
program verification
defect correction
