article

Free access

The synthesis of loop predicates

Author:

Ben WegbreitAuthors Info & Claims

Communications of the ACM, Volume 17, Issue 2

Pages 102 - 113

https://doi.org/10.1145/360827.360850

Published: 01 February 1974 Publication History

PDF eReader

Abstract

Current methods for mechanical program verification require a complete predicate specification on each loop. Because this is tedious and error prone, producing a program with complete, correct predicates is reasonably difficult and would be facilitated by machine assistance. This paper discusses techniques for mechanically synthesizing loop predicates. Two classes of techniques are considered: (1) heuristic methods which derive loop predicates from boundary conditions and/or partially specified inductive assertions: (2) extraction methods which use input predicates and appropriate weak interpretations to obtain certain classes of loop predicates by an evaluation on the weak interpretation.

References

[1]

Cocke, J., and Schwartz, J.T. Programming Languages and Their Compilers. Courant Inst. of Math. Sci., New York U., N. Y., Apr. 1970.

Digital Library

Google Scholar

[2]

Cooper, D.C. Programs for mechanical program verification. In Machine Intelligence 6, American Elsevier, New York, 1971, pp. 43-59.

Google Scholar

[3]

Deutsch, L.P. An interactive program verifier. Ph.D. Th., Dep. Comput, Sci., U. of California, Berkeley, Calif., June 1973.

Google Scholar

[4]

Elspas, B., Green, M.W., Levitt, K.N., and Waldinger, R. J. Research in interactive program-proving techniques. SRI, Menlo Park, Calif., May 1972.

Google Scholar

[5]

Elspas, B., Levitt, K.N., Waldinger, R.J., and Waksman, A. An assessment of techniques for proving programs correct. Computing Surveys 4, 2 (June 1972), 97-147.

Digital Library

Google Scholar

[6]

Floyd, R. J. Assigning meanings to programs. In Proc. of a Symposium in Applied Mathematics, Vat. 19, J.T. Schwartz (Ed.), AMS, 1967, pp. 19-32.

Crossref

Google Scholar

[7]

Hewitt, C. PLANNER: A language for proving theorems and manipulating models in a robot. Ph.D. Th., MIT, Dep. Math., Jan. 1971.

Google Scholar

[8]

Katz, S.M., and Manna, Z. A heuristic approach to program verification. Proc. 3rd Internat. Joint Conf. on Artif. Intel., Aug. 1973, pp. 500-512.

Digital Library

Google Scholar

[9]

King, J. A program verifier Doc. diss., Comput. Sci. Dep., Carnegie-Mellon U., Pittsburgh, Pa., 1969

Digital Library

Google Scholar

[10]

London, R.L. The current state of proving programs correct. Proc. ACM 25th Ann. Conf., 1972, pp. 39-46.

Digital Library

Google Scholar

[11]

McDermott, D.V., and Sussman, G.J. The CONNIVER reference manual. Memo No. 259, MIT, A.I. Lab., May 1972.

Google Scholar

[12]

Rulifson, J.F., Derksen, J.A., and Waldinger, R.J. QA4: A procedural calculus for intuitive reasoning. Tech. Note 73, SRI, Nov. 1972.

Google Scholar

[13]

Wegbreit, B. Property extraction in well-founded property sets. Tech. Rep., Cent. for Res. in Comput. Tech. Harvard U., Cambridge, Mass., Feb., 1973.

Google Scholar

[14]

Vegbreit, B. Heuristic methods for mechanically deriving inductive assertions. Proc. 3rd Internat. Joint Conf. on Artif. Intel., Aug. 1973, pp. 524-536.

Google Scholar

Cited By

View all

Valle RDonzé AFremont DAkkaya ISeshia SFreed AWessel D(2016)Specification Mining for Machine Improvisation with Formal SpecificationsComputers in Entertainment10.1145/296750414:3(1-20)Online publication date: 31-Dec-2016
https://dl.acm.org/doi/10.1145/2967504
Di Vito B(2016)Deductive evaluationProceedings of the 4th FME Workshop on Formal Methods in Software Engineering10.1145/2897667.2898414(1-7)Online publication date: 14-May-2016
https://dl.acm.org/doi/10.1145/2897667.2898414
(2016)Identifying locations from geospatial trajectoriesJournal of Computer and System Sciences10.1016/j.jcss.2015.10.00582:4(566-581)Online publication date: 1-Jun-2016
https://dl.acm.org/doi/10.1016/j.jcss.2015.10.005
Show More Cited By

Index Terms

The synthesis of loop predicates

Recommendations

A synthesizer of inductive assertions

Most current methods for mechanical program verification require a complete inductive assertion on each loop. As this is tedious and error prone, producing a program with complete, correct assertions is moderately difficult. This paper describes a ...
A Mechanical Analysis of Program Verification Strategies

We analyze three proof strategies commonly used in deductive verification of deterministic sequential programs formalized with operational semantics. The strategies are (i) stepwise invariants , (ii) clock functions , and (iii) inductive assertions . ...
Consequence Verification of Flowcharts

A common basis is presented, for Floyd's method of inductive assertions and for the subgoal induction method of Morris and Wegbreit. This basis is provided by consequence verification, a method for verifying logic programs. We connect flowcharts with ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Communications of the ACM Volume 17, Issue 2

Feb. 1974

54 pages

ISSN:0001-0782

EISSN:1557-7317

DOI:10.1145/360827

Editor:
Robert L. Ashenhurst
Univ. of Chicago, Chicago, IL

Issue’s Table of Contents

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 February 1974

Published in CACM Volume 17, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

119
Total Citations
View Citations
717
Total Downloads

Downloads (Last 12 months)125
Downloads (Last 6 weeks)17

Reflects downloads up to 05 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Valle RDonzé AFremont DAkkaya ISeshia SFreed AWessel D(2016)Specification Mining for Machine Improvisation with Formal SpecificationsComputers in Entertainment10.1145/296750414:3(1-20)Online publication date: 31-Dec-2016
https://dl.acm.org/doi/10.1145/2967504
Di Vito B(2016)Deductive evaluationProceedings of the 4th FME Workshop on Formal Methods in Software Engineering10.1145/2897667.2898414(1-7)Online publication date: 14-May-2016
https://dl.acm.org/doi/10.1145/2897667.2898414
(2016)Identifying locations from geospatial trajectoriesJournal of Computer and System Sciences10.1016/j.jcss.2015.10.00582:4(566-581)Online publication date: 1-Jun-2016
https://dl.acm.org/doi/10.1016/j.jcss.2015.10.005
Chu VWong RChen FFong SHung P(2016)Self-regularized causal structure discovery for trajectory-based networksJournal of Computer and System Sciences10.1016/j.jcss.2015.10.00482:4(594-609)Online publication date: 1-Jun-2016
https://dl.acm.org/doi/10.1016/j.jcss.2015.10.004
Mehrabi ESchost É(2016)A softly optimal Monte Carlo algorithm for solving bivariate polynomial systems over the integersJournal of Complexity10.1016/j.jco.2015.11.00934:C(78-128)Online publication date: 1-Jun-2016
https://dl.acm.org/doi/10.1016/j.jco.2015.11.009
Moczurad MZgliczyński PZwonek W(2016)New lower bound estimates for quadratures of bounded analytic functionsJournal of Complexity10.1016/j.jco.2015.11.00734:C(50-67)Online publication date: 1-Jun-2016
https://dl.acm.org/doi/10.1016/j.jco.2015.11.007
De Benedetti ERonchi Della Rocca S(2016)A type assignment for λ-calculus complete both for FPTIME and strong normalizationInformation and Computation10.1016/j.ic.2015.12.012248:C(195-214)Online publication date: 1-Jun-2016
https://dl.acm.org/doi/10.1016/j.ic.2015.12.012
(2016)A semantic account of strong normalization in linear logicInformation and Computation10.1016/j.ic.2015.12.010248:C(104-129)Online publication date: 1-Jun-2016
https://dl.acm.org/doi/10.1016/j.ic.2015.12.010
Bonfante GKahle RMarion JOitavem I(2016)Two function algebras defining functions in NC k boolean circuitsInformation and Computation10.1016/j.ic.2015.12.009248:C(82-103)Online publication date: 1-Jun-2016
https://dl.acm.org/doi/10.1016/j.ic.2015.12.009
Cavoretto RDe Rossi APerracchione E(2016)Efficient computation of partition of unity interpolants through a block-based searching techniqueComputers & Mathematics with Applications10.1016/j.camwa.2016.04.02171:12(2568-2584)Online publication date: 1-Jun-2016
https://dl.acm.org/doi/10.1016/j.camwa.2016.04.021
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

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

Abstract

References

Cited By

Index Terms

Recommendations

A synthesizer of inductive assertions

A Mechanical Analysis of Program Verification Strategies

Consequence Verification of Flowcharts

Comments

Information

Published In

Publisher

Publication History

Permissions

Check for updates

Author Tags

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations