article

Free access

Inductive methods for proving properties of programs

Authors:

Jean VuilleminAuthors Info & Claims

ACM SIGPLAN Notices, Volume 7, Issue 1

Pages 27 - 50

https://doi.org/10.1145/942578.807070

Published: 01 January 1972 Publication History

Abstract

We have two main purposes in this paper. First, we clarify and extend known results about computation of recursive programs, emphasizing the difference between the theoretical and practical approaches. Secondly, we present and examine various known methods for proving properties of recursive programs. We discuss in detail two powerful inductive methods, computational induction and structural induction, illustrating their applications by various examples. We also briefly discuss some other related methods.

Our aim in this work is to introduce inductive methods to as wide a class of readers as possible and to demonstrate their power as practical techniques. We ask the forgiveness of our more theoretical-minded colleagues for our occasional choice of clarity over precision.

References

[1]

R. M. Burstall, "Proving Properties of Programs by Structural Induction". Computer Journal, Vol. 12, pp. 41-48 (1969).

[2]

J. M. Cadiou, "Recursive Definitions of Partial Functions and Their Computations", Ph.D. Thesis, Computer Science Department, Stanford University (to appear).

Digital Library

[3]

J. W. deBakker and Dana Scott, "A Theory of Programs", Unpublished memo., August 1969.

[4]

R.W. Floyd, "Assigning Meanings to Programs". In Proceedings of a Symposium in Applied Mathematics, Vol. 19. Mathematical Aspects of Computer Science, pp. 19-32 (ed. J. T. Schwartz). Providence, Rhode Island, American Mathematical Society (1967).

[5]

S. C. Kleene, Introduction to Meta-mathematics, D. Van Nostrand, Princeton, New Jersey (1950).

[6]

Zohar Manna and Amir Pnueli, "Formalization of Properties of Functional Programs", JACM, Vol. 17, No. 3 (July 1970), pp. 555-569.

Digital Library

[7]

John McCarthy, "Towards a Mathematical Science of Computation", In Information Processing; Proceedings of IFIP 62, pp. 21-28, (ed. C. M. Popplewell). Amsterdam, North Holland (1963).

[8]

John McCarthy, "A Basis for a Mathematical Theory of Computation". In Computer Programming and Formal Systems, pp. 33-70 (eds. P. Braffort and D. Hirschberg). Amsterdam, North Holland (1963). Also in Proceedings of the Western Joint Computer Conference, pp. 225-238. New York, Spartan Books (1961).

[9]

John McCarthy and J. A. Painter, "Correctness of a Compiler for Arithmetic Expressions". In Proceedings of a Symposium in Applied Mathematics, Vol. 19. Mathematical Aspects of Computer Science, pp. 33-41. (ed. J. T. Schwartz). Providence, Rhode Island, American Mathematical Society (1967).

[10]

Robin Milner, "Logic for Computable Functions - Description of a Machine Implementation", Computer Science report, Stanford University (to appear).

Digital Library

[11]

Robin Milner, "Implementation and Applications of Scott's Logic for Computable Functions", presented at the conference Proving Assertions About Programs, Las Cruces, New Mexico (January 1972).

Digital Library

[12]

Marvin Minsky, Computation - Finite and Infinite Machines, Prentice-Hall (1967).

Digital Library

[13]

James H. Morris, "Lambda-Calculus Models of Programming Languages", Ph.D. Thesis, Project MAC, M.I.T. (MAC-TR-57). December 1968.

[14]

James H. Morris, "Another Recursion Induction Principle", CACM, Vol. 14, No. 5, pp. 351-354 (May 1971).

Digital Library

[15]

Peter Naur, "Proof of Algorithms by General Snapshots", BIT, Vol. 6, pp. 310-316 (1966).

Digital Library

[16]

David Park, "Fixpoint Induction and Proofs of Program Properties". In Machine Intelligence 5 (eds. B. Meltzer and D. Michie), Edinburgh University Press (1969).

[17]

Dana Scott, "A Type Theoretical Alternative to ISWIM, CUCH, OWHY". Unpublished notes, Oxford University (1969).

[18]

Dana Scott, "Outline of a Mathematical Theory of Computation", Oxford University Computing Laboratory, Programming Research Group, Technical Monograph PRG-2 (November 1970).

[19]

Jean Vuillemin, "Proof Techniques for Recursive Programs", Ph.D. Thesis, Computer Science Department, Stanford University (to appear).

Digital Library

Cited By

Goossens K(2005)Structure and behaviour in hardware verificationHigher Order Logic Theorem Proving and Its Applications10.1007/3-540-57826-9_126(75-88)Online publication date: 31-May-2005
https://doi.org/10.1007/3-540-57826-9_126
Rosendahl M(2005)Abstract interpretation using attribute grammarsAttribute Grammars and their Applications10.1007/3-540-53101-7_11(143-156)Online publication date: 31-May-2005
https://doi.org/10.1007/3-540-53101-7_11
Coriat M(1995)Formal specification of software critical systems with agents1995 IEEE Aerospace Applications Conference. Proceedings10.1109/AERO.1995.468939(317-336)Online publication date: 1995
https://doi.org/10.1109/AERO.1995.468939
Show More Cited By

Index Terms

Inductive methods for proving properties of programs
1. Computing methodologies
  1. Machine learning
    1. Machine learning approaches
      1. Logical and relational learning
        Inductive logic learning
2. Theory of computation
  1. Theory and algorithms for application domains
    1. Machine learning theory
      1. Inductive inference

Recommendations

Inductive methods for proving properties of programs

There are two main purposes in this paper: first, clarification and extension of known results about computation of recursive programs, with emphasis on the difference between the theoretical and practical approaches; second, presentation and ...
Inductive methods for proving properties of programs
Proceedings of ACM conference on Proving assertions about programs

We have two main purposes in this paper. First, we clarify and extend known results about computation of recursive programs, emphasizing the difference between the theoretical and practical approaches. Secondly, we present and examine various known ...
Inductive methods for proving properties of programs
Proceedings of ACM conference on Proving assertions about programs

We have two main purposes in this paper. First, we clarify and extend known results about computation of recursive programs, emphasizing the difference between the theoretical and practical approaches. Secondly, we present and examine various known ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 7, Issue 1

Proceedings of ACM conference on Proving assertions about programs

January 1972

211 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/942578

Issue’s Table of Contents

Proceedings of ACM conference on Proving assertions about programs
January 1972
215 pages
ISBN:9781450378918
DOI:10.1145/800235

Copyright © 1972 Authors.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 1972

Published in SIGPLAN Volume 7, Issue 1

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

58
Total Citations
View Citations
679
Total Downloads

Downloads (Last 12 months)89
Downloads (Last 6 weeks)13

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Goossens K(2005)Structure and behaviour in hardware verificationHigher Order Logic Theorem Proving and Its Applications10.1007/3-540-57826-9_126(75-88)Online publication date: 31-May-2005
https://doi.org/10.1007/3-540-57826-9_126
Rosendahl M(2005)Abstract interpretation using attribute grammarsAttribute Grammars and their Applications10.1007/3-540-53101-7_11(143-156)Online publication date: 31-May-2005
https://doi.org/10.1007/3-540-53101-7_11
Coriat M(1995)Formal specification of software critical systems with agents1995 IEEE Aerospace Applications Conference. Proceedings10.1109/AERO.1995.468939(317-336)Online publication date: 1995
https://doi.org/10.1109/AERO.1995.468939
COUSOT P(1990)Methods and Logics for Proving ProgramsFormal Models and Semantics10.1016/B978-0-444-88074-1.50020-2(841-993)Online publication date: 1990
https://doi.org/10.1016/B978-0-444-88074-1.50020-2
Büchi JMahr BSiefkes D(1990)Recursive Definition and Complexity of Functions Over Arbitrary Data StructuresThe Collected Works of J. Richard Büchi10.1007/978-1-4613-8928-6_35(641-663)Online publication date: 1990
https://doi.org/10.1007/978-1-4613-8928-6_35
Case JMoelius III S(2011)Properties Complementary to Program Self-ReferenceFundamenta Informaticae10.5555/2361502.2361503111:3(281-311)Online publication date: 1-Aug-2011
https://dl.acm.org/doi/10.5555/2361502.2361503
Case JMoelius S(2009)Independence results for n-ary recursion theoremsProceedings of the 17th international conference on Fundamentals of computation theory10.5555/1789494.1789501(38-49)Online publication date: 2-Sep-2009
https://dl.acm.org/doi/10.5555/1789494.1789501
Case JMoelius S(2009)Independence Results for n-Ary Recursion TheoremsFundamentals of Computation Theory10.1007/978-3-642-03409-1_5(38-49)Online publication date: 2009
https://doi.org/10.1007/978-3-642-03409-1_5
Hewitt CBishop PSteiger RGreif ISmith BMatson THale R(2005)Behavioral semantics of nonrecursive control structuresProgramming Symposium10.1007/3-540-06859-7_147(385-407)Online publication date: 20-Jun-2005
https://doi.org/10.1007/3-540-06859-7_147
Noonan RPanton D(2005)Structured recursive programmingProgramming Symposium10.1007/3-540-06859-7_126(81-87)Online publication date: 20-Jun-2005
https://doi.org/10.1007/3-540-06859-7_126
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents