PROVING PROPERTIES OF PROGRAMS BY STRUCTURAL INDUCTION

被引：102

作者：

BURSTALL, RM

机构：

[1] Department of Machine Intelligence and Perception, University of Edinburgh

来源：

COMPUTER JOURNAL | 1969年 / 12卷 / 01期

关键词：

D O I：

10.1093/comjnl/12.1.41

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

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. © 1969 The British Computer Society.

引用

页码：41 / &

共 17 条

[1] Barron D. W., 1966, ADV PROGRAMMING NONN, P49
[2] BROOKER RA, 1967, MACHINE INTELLIGENCE, V1, P229
[3] BURSTALL RM, 1968, MACHINE INTELLIGENCE, V2, P3
[4] COHN PM, 1965, UNIVERSAL ALGEBRA
[5] COLLINS NL, 1967, MACHINE INTELLIGE ED, V1, P229
[6] EQUIVALENCE OF CERTAIN COMPUTATIONS
COOPER, DC
[J]. COMPUTER JOURNAL, 1966, 9 (01) : 45 - &
[7] Curry H.B., 1958, COMBINATORY LOGIC
[8] DALE E, 1968, MACHINE INTELLIGE ED, V2, P3
[9] FOX L, 1966, ADVANCES PROGRAMM ED, P49
[10] KAPLAN DM, 1967, 48 STANF U DEP COMP

← 1 2 →