Proving Properties of Programs by Structural Induction
Proving Properties of Programs by Structural Induction
复制标题
通过结构归纳证明程序的性质
DOI：
--
复制
发表时间：
1969
期刊：
影响因子：
--
通讯作者：
R. Burstall
中科院分区：
文献类型：
--
作者：
R. Burstall
本文讨论了证明有关程序的定理的结构归纳技术。该技术与递归归纳密切相关，但利用了程序处理的数据结构的归纳定义。它用递归处理程序，但没有作业或跳跃。建议对Landin功能编程语言ISWIM进行一些句法扩展，这使得对数据结构进行操纵并开发有关此类程序的证据变得更加容易。给出了两个示例证明以演示该技术，一种用于树的排序算法，一个用于表达式的简单编译器。 （1968年4月首次收到，并以修订的表格获得1968年8月）
This paper discusses the technique of structural induction for proving theorems about programs. This technique is closely related to recursion induction but makes use of the inductive definition of the data structures handled by the programs. It treats programs with recursion but without assignments or jumps. Some syntactic extensions to Landin's functional programming language ISWIM are suggested which make it easier to program the manipulation of data structures and to develop proofs about such programs. Two sample proofs are given to demonstrate the technique, one for a tree sorting algorithm and one for a simple compiler for expressions. (First received April 1968 and in revised form August 1968)