The synthesis of loop predicates
The synthesis of loop predicates
复制标题
DOI：
10.1145/360827.360850
复制
发表时间：
1974-02
期刊：
影响因子：
--
通讯作者：
B. Wegbreit
中科院分区：
文献类型：
--
作者：
B. Wegbreit
当前的机械程序验证方法需要对每个回路进行完整的谓词规范。因为这是乏味的和容易出错的，所以产生一个具有完整的、正确的谓词的程序是相当困难的，并且将通过机器辅助来促进。本文讨论机械合成循环谓词的技术。考虑了两类技术：（1）启发式方法，从边界条件和/或部分指定的归纳断言导出循环谓词;（2）提取方法，使用输入谓词和适当的弱解释，通过对弱解释的评估来获得某些类别的循环谓词。
Current methods for mechanical program verification require a complete predicate specification on each loop. Because this is tedious and error prone, producing a program with complete, correct predicates is reasonably difficult and would be facilitated by machine assistance. This paper discusses techniques for mechanically synthesizing loop predicates. Two classes of techniques are considered: (1) heuristic methods which derive loop predicates from boundary conditions and/or partially specified inductive assertions: (2) extraction methods which use input predicates and appropriate weak interpretations to obtain certain classes of loop predicates by an evaluation on the weak interpretation.