PROGRAM INVERSION - MORE THAN FUN

被引：28

作者：

CHEN, W ^{[1
]}

UDDING, JT ^{[1
]}

机构：

[1] STATE UNIV GRONINGEN,DEPT MATH & COMP SCI,9700 AB GRONINGEN,NETHERLANDS

来源：

SCIENCE OF COMPUTER PROGRAMMING | 1990年 / 15卷 / 01期

关键词：

D O I：

10.1016/0167-6423(90)90042-C

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We introduce proof rules for inverting a program. We derive an algorithm to compute the preorder and inorder traversals of a binary tree. Subsequently, we invert this algorithm to arrive at an algorithm to construct a tree from its preorder and inorder traversals. We prove this program correct using the proof rules for inversion rather than directly. Since a proper formulation of a provable invariant of this program appears to be quite awkward, this example reinforces the view that program inversion is a useful technique and more than fun. © 1990.

引用

页码：1 / 13

页数：13