[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
10.1145/512976.512993acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
Article
Free access

An assertion language for data structures

Published: 01 January 1975 Publication History

Abstract

In this paper we wish to consider the problem of proving assertions about programs that construct and alter arbitrarily complex data structures. In recent years several papers have been written on the subject of proving assertions about such programs; however, the class of data structures considered has generally been a proper sub-class of the class of all data structures, such as the classes of linear lists or trees. [Burstall 1972] discusses the problem of what he calls Distinct Non-repeating Lists and Distinct Non-repeating Trees. [Kowaltowski 1973] extends Burstall's approach. His approach is likewise basically tree-oriented but is applicable to more general data structures. [Laventhal 1974] restricts his attention to 'simple singly-linked lists', noting the problem of providing 'a complete framework for correctness proofs' if one attempts to handle very general data structures. [Morris 1972] discusses the question of designing a programming language for general data structures in order to facilitate verification of programs written in such a language. [Standish 1973] provides a set of axioms for the class of data structures in which, for instance, two data structures are equal iff they are component-wise equal.

References

[1]
Burstall, R. M., Some Techniques for Proving Correctness of Programs which Alter Data Structures. Machine Intelligence 7, 1972.
[2]
Cook, S. A., Axiomatic and Interpretive Semantics for an Algol Fragment. Course notes for CSC 2409S, Dept. of Computer Science, University of Toronto, March 1974.
[3]
Davis, M., Computability and Unsolvability. McGraw-Hill, 1958.
[4]
Hoare, C. A. R., An Axiomatic Basis for Computer Programming. Communications of the ACM, October 1969.
[5]
Kowaltowski, T., Correctness of Programs Manipulating Data Structure. Memorandum No. ERL-M404, Electronics Research Laboratory, University of California, Berkeley, September 1973.
[6]
Laventhal, M. S., Verification of Programs Operating on Structured Data. M.Sc. Thesis, M.I.T., February 1974.
[7]
Morris, J. H., Verification Oriented Language Design. Technical Report 7, Dept. of Computer Science, University of California, Berkeley, December 1972.
[8]
Rosenberg, A. L., Data Graphs and Addressing Schemes. Journal of Computer and System Sciences, June 1971, pp. 193-238.
[9]
Standish, T. A., Data Structures: An Axiomatic Approach. Automatic Programming Memo 3, Bolt, Beranek and Newman Inc., August 1973.

Cited By

View all
  • (2017)Property-Directed Inference of Universal Invariants or Proving Their AbsenceJournal of the ACM10.1145/302218764:1(1-33)Online publication date: 29-Mar-2017
  • (2013)Scope Logic: An Extension to Hoare Logic for Pointers and Recursive Data StructuresTheoretical Aspects of Computing – ICTAC 201310.1007/978-3-642-39718-9_24(409-426)Online publication date: 2013
  • (2005)Theory of data structures by relational and graph grammarsAutomata, Languages and Programming10.1007/3-540-08342-1_31(391-411)Online publication date: 24-May-2005
  • Show More Cited By

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences
POPL '75: Proceedings of the 2nd ACM SIGACT-SIGPLAN symposium on Principles of programming languages
January 1975
242 pages
ISBN:9781450373517
DOI:10.1145/512976
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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 1975

Permissions

Request permissions for this article.

Check for updates

Qualifiers

  • Article

Acceptance Rates

POPL '75 Paper Acceptance Rate 23 of 100 submissions, 23%;
Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)56
  • Downloads (Last 6 weeks)6
Reflects downloads up to 14 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2017)Property-Directed Inference of Universal Invariants or Proving Their AbsenceJournal of the ACM10.1145/302218764:1(1-33)Online publication date: 29-Mar-2017
  • (2013)Scope Logic: An Extension to Hoare Logic for Pointers and Recursive Data StructuresTheoretical Aspects of Computing – ICTAC 201310.1007/978-3-642-39718-9_24(409-426)Online publication date: 2013
  • (2005)Theory of data structures by relational and graph grammarsAutomata, Languages and Programming10.1007/3-540-08342-1_31(391-411)Online publication date: 24-May-2005
  • (2005)Safety and liveness in concurrent pointer programsProceedings of the 4th international conference on Formal Methods for Components and Objects10.1007/11804192_14(280-312)Online publication date: 1-Nov-2005
  • (2004)Who is pointing when to whom?Proceedings of the 24th international conference on Foundations of Software Technology and Theoretical Computer Science10.1007/978-3-540-30538-5_21(250-262)Online publication date: 16-Dec-2004
  • (2001)The pointer assertion logic engineACM SIGPLAN Notices10.1145/381694.37885136:5(221-231)Online publication date: 1-May-2001
  • (2001)The pointer assertion logic engineProceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation10.1145/378795.378851(221-231)Online publication date: 20-Jun-2001
  • (2001)Alias Types for Recursive Data StructuresTypes in Compilation10.1007/3-540-45332-6_7(177-206)Online publication date: 13-Jun-2001
  • (1990)Exposing graph uniformities via algebraic specificationMathematical Systems Theory10.1007/BF0209077723:1(227-244)Online publication date: Dec-1990
  • (1977)The taming of the pointerACM SIGPLAN Notices10.1145/954639.95464312:7(60-74)Online publication date: 1-Jul-1977
  • 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

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media