More Web Proxy on the site http://driver.im/

article

Free access

Test data as an aid in proving program correctness

Author:

Matthew GellerAuthors Info & Claims

Communications of the ACM, Volume 21, Issue 5

Pages 368 - 375

https://doi.org/10.1145/359488.359495

Published: 01 May 1978 Publication History

Abstract

Proofs of program correctness tend to be long and tedious, whereas testing, though useful in detecting errors, usually does not guarantee correctness. This paper introduces a technique whereby test data can be used in proving program correctness. In addition to simplifying the process of providing correctness, this method simplifies the process of providing accurate specification for a program. The applicability of this technique to procedures and recursive programs is demonstrated.

References

[1]

Boyer, R.S., Elspas, B., and Levitt, K. SELECT--a formal system for testing and debugging programs by symbolic execution. Proc. Int. Conf. on Reliable Software, 1975, pp. 234-245.

Digital Library

[2]

Boyer, R.S., and Moore, J.L. Proving theorems about LISP functions. J. ACM 22, 1 (Jan. 1975), 129-144.

Digital Library

[3]

Burstall, R.M. Proving properties of programs by structural induction. Comptr. J. 12 (1969), 41-48.

[4]

Clarke, L. A system to generate test data and symbolically execute programs. 1EEE Trans. Software Eng. 2, 3 (1976), 227-231.

[5]

Dabl, O.-J., Dijkstra, E.W., and Hoare, C.A.R. Structured Programming. Academic Press, London and New York, 1972.

[6]

Floyd, R.W. Assigning meanings to programs. Proceedings of a Symposium in Applied Mathematics, Vol. 19, J. T. Schwartz, Ed., Amer. Math. Soc., 1967, pp. 19-32.

[7]

Goodenough, J.B., and Gerhart, S.L. Toward a theory of test data selection. Proc. Int. Conf. on Reliable Software, 1975, pp. 493-510.

Digital Library

[8]

Henderson, P. Finite state modelling in program development. Proc. Int. Conf. on Reliable Software, 1975, pp. 221-227.

Digital Library

[9]

Hoare, C.A.R. Proof of correctness of data representation. Acta lnformatica 1, 4 (1972), 271-281.

[10]

Howden, W.E. Reliability of the path analysis testing strategy. 1EEE Trans. Software Eng. 2, 3 (1976), 208-214.

[11]

Katz, S.M., and Manna, Z. Logical analysis of programs. The Weizmann Inst. of Sci., 1974.

[12]

King, J.C. A new approach to program testing. Proc. Int. Conf. on Reliable Software, 1975, pp. 228-233.

Digital Library

[13]

Liskov, B.H., and Zilles, S.N. Specification techniques for data abstractions. IEEE Trans. on Software Eng. 1, 1 (March 1975), 7-19.

[14]

London, R.L. A view of program verification. Proc. Int. Conf. on Reliable Software, 1975, 534-545.

Digital Library

[15]

Manna, Z., Ness, S., and VuiUemin, J. Inductive methods for proving properties of programs. Comm. A CM 16, 8 (Aug. 1973), 491-502.

Digital Library

[16]

Miller, E.F. Jr., and Melton, R.A. Automated generation of testcase datasets. Proc. Int. Conf. on Reliable Software, 1975, pp. 51-58.

Digital Library

[17]

Robinson, L., and Levitt, K. Proof techniques for hierarchically structured programs. Standord Res. Inst., Menlo Park, Calif., 1975.

[18]

Sintzoff, J. Calculating properties of programs by valuations on specific models. Proc. ACM Conf. on Proving Assertions About Programs, Jan., 1972, pp. 203-207.

Digital Library

[19]

Sites, R. Proving that computer programs terminate cleanly. TR STAN-CS-74-418, Stanford, U., Stanford, Calif., 1974.

[20]

Wegbreit, B. The synthesis of loop predicates. Comm. ACM 16, 2 (Feb. 1974), 102-112.

Digital Library

Cited By

Chen TKuo FLiu HPoon PTowey DTse TZhou Z(2018)Metamorphic TestingACM Computing Surveys10.1145/314356151:1(1-27)Online publication date: 4-Jan-2018
https://dl.acm.org/doi/10.1145/3143561
Gaudel M(2011)Checking models, proving programs, and testing systemsProceedings of the 5th international conference on Tests and proofs10.5555/2025936.2025937(1-13)Online publication date: 30-Jun-2011
https://dl.acm.org/doi/10.5555/2025936.2025937
Chen TTse TZhou Z(2011)Semi-ProvingIEEE Transactions on Software Engineering10.1109/TSE.2010.2337:1(109-125)Online publication date: 1-Jan-2011
https://dl.acm.org/doi/10.1109/TSE.2010.23
Show More Cited By

Index Terms

Test data as an aid in proving program correctness
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Software defect analysis
        Software testing and debugging
  2. Software organization and properties
    1. Software functional properties
      1. Correctness
2. Theory of computation
  1. Logic
    1. Proof theory

Recommendations

Test data as an aid in proving program correctness
POPL '76: Proceedings of the 3rd ACM SIGACT-SIGPLAN symposium on Principles on programming languages

Proofs of program correctness tend to be long and tedious whereas testing, though useful in detecting errors, usually does not guarantee correctness. This paper introduces a technique whereby test data can be used in proving program correctness. In ...
A view of program verification
Proceedings of the international conference on Reliable software

One person's perspectives of program verification and its relation to some aspects of reliable software are presented. The main verification method of inductive assertions is illustrated with several variations of one detailed example; a second example ...
A view of program verification
International Conference on Reliable Software

One person's perspectives of program verification and its relation to some aspects of reliable software are presented. The main verification method of inductive assertions is illustrated with several variations of one detailed example; a second example ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Communications of the ACM

Communications of the ACM Volume 21, Issue 5

May 1978

81 pages

ISSN:0001-0782

EISSN:1557-7317

DOI:10.1145/359488

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

Issue’s Table of Contents

Copyright © 1978 ACM.

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 May 1978

Published in CACM Volume 21, Issue 5

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

33
Total Citations
View Citations
513
Total Downloads

Downloads (Last 12 months)98
Downloads (Last 6 weeks)7

Reflects downloads up to 12 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Chen TKuo FLiu HPoon PTowey DTse TZhou Z(2018)Metamorphic TestingACM Computing Surveys10.1145/314356151:1(1-27)Online publication date: 4-Jan-2018
https://dl.acm.org/doi/10.1145/3143561
Gaudel M(2011)Checking models, proving programs, and testing systemsProceedings of the 5th international conference on Tests and proofs10.5555/2025936.2025937(1-13)Online publication date: 30-Jun-2011
https://dl.acm.org/doi/10.5555/2025936.2025937
Chen TTse TZhou Z(2011)Semi-ProvingIEEE Transactions on Software Engineering10.1109/TSE.2010.2337:1(109-125)Online publication date: 1-Jan-2011
https://dl.acm.org/doi/10.1109/TSE.2010.23
Gaudel M(2011)Checking Models, Proving Programs, and Testing SystemsTests and Proofs10.1007/978-3-642-21768-5_1(1-13)Online publication date: 2011
https://doi.org/10.1007/978-3-642-21768-5_1
Leavens GRoman GSullivan K(2010)The future of library specificationProceedings of the FSE/SDP workshop on Future of software engineering research10.1145/1882362.1882407(211-216)Online publication date: 7-Nov-2010
https://dl.acm.org/doi/10.1145/1882362.1882407
Huang J(2008)BibliographySoftware Error Detection through Testing and Analysis10.1002/9780470464076.biblio(237-251)Online publication date: 28-Oct-2008
https://doi.org/10.1002/9780470464076.biblio
Hamlet D(2005)Invariants and state in testing and formal methodsProceedings of the 6th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering10.1145/1108792.1108806(48-51)Online publication date: 5-Sep-2005
https://dl.acm.org/doi/10.1145/1108792.1108806
Hamlet D(2005)Invariants and state in testing and formal methodsACM SIGSOFT Software Engineering Notes10.1145/1108768.110880631:1(48-51)Online publication date: 5-Sep-2005
https://dl.acm.org/doi/10.1145/1108768.1108806
Hähnle RWallenburg A(2004)Using a Software Testing Technique to Improve Theorem ProvingFormal Approaches to Software Testing10.1007/978-3-540-24617-6_3(30-41)Online publication date: 2004
https://doi.org/10.1007/978-3-540-24617-6_3
Dybjer PQiao Haiyan Takeyama M(2003)Verifying Haskell programs by combining testing and provingThird International Conference on Quality Software, 2003. Proceedings.10.1109/QSIC.2003.1319111(272-279)Online publication date: 2003
https://doi.org/10.1109/QSIC.2003.1319111
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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents