Logo image
Primitive recursive program transformation
Conference proceeding   Open access

Primitive recursive program transformation

R Boyer, J Moore and R Shostak
Proceedings of the 3rd ACM SIGACT-SIGPLAN symposium on principles on programming languages, pp 171-174
01 Jan 1976
url
https://doi.org/10.1145/800168.811550View
Published, Version of Record (VoR) Open

Abstract

Flowcharts LISP Program verification Structural induction Theorem proving
We describe how to transform certain flowchart programs into equivalent explicit primitive recursive programs. The input/output correctness conditions for the transformed programs are more amenable to proof than the verification conditions for the corresponding flowchart programs. In particular, the transformed correctness conditions can often be verified automatically by the theorem prover developed by Boyer and Moore [1].

Metrics

17 Record Views
2 citations in Scopus

Details

Logo image