This paper proposes a framework facilitating the automatic analysis on inductive properties for recursive data structures. This work has three main parts. First, the analysis of heap-manipulating programs is simplified by classifying inductive properties of recursive data structures into two classifications, each of them is handled with observed patterns. Second, a slicing and splicing technique, in which data structures are first sliced into several parts and these parts are further spliced into new data s...
霍尔式的程序证明(Hoare-style program verification)是保证代码功能正确性的重要手段.然而,实现证明过程的自动化却受到两个主要问题的制约,分别对应于霍尔逻辑[24](Hoare logic)中的两个规则,即循环规则(ruleof iteration)和赋值规则(axiom schema of assignment).第一,循环
| 
推荐 
点击下列相关研究机构和相关文献作者，可以直接查到这些机构和作者被《中国知识资源总库》收录的其它文献，使您全面了解该机构和该作者的研究动态和历史。
