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

Article

A Trace Model for Pointers and Objects

Authors:

C. A. R. Hoare,

He JifengAuthors Info & Claims

ECOOP '99: Proceedings of the 13th European Conference on Object-Oriented Programming

Pages 1 - 17

Published: 14 June 1999 Publication History

Abstract

Object-oriented programs [Dahl, Goldberg, Meyer] are notoriously prone to the following kinds of error, which could lead to increasingly severe problems in the presence of tasking 1. Following a null pointer 2. Deletion of an accessible object 3. Failure to delete an inaccessible object 4. Interference due to equality of pointers 5. Inhibition of optimisation due to fear of (4)

Type disciplines and object classes are a great help in avoiding these errors. Stronger protection may be obtainable with the help of assertions, particularly invariants, which are intended to be true before and after each call of a method that updates the structure of the heap. This note introduces a mathematical model and language for the formulation of assertions about objects and pointers, and suggests that a graphical calculus [Curtis, Lowe] may help in reasoning about program correctness. It deals with both garbage-collected heaps and the other kind. The theory is based on a trace model of graphs, using ideas from process algebra; and our development seeks to exploit this analogy as a unifying principle.

References

[1]

M. Abadi and L. Cardelli. A theory of objects. Springer (1998).

[2]

L. Cardelli. A semantics of multiple inheritance. Information and Computation 76: 138-164 (1988).

[3]

W. Cook and J. Palsberg. A denotational semantics of inheritance and its correctness. Information and Computation 114(2), 329-350 (1994).

[4]

S. Curtis and G. Lowe, A graphical calculus. In B. Möller (ed) Mathematics of Program Construction LNCS 947 Springer (1995).

[5]

O. Dahl and K. Nygaard. Simula, an Algol-based simulation language. Communications of the ACM 9(9) 671-678 (1966).

[6]

A. Goldberg and D. Robson. Smalltalk-80. The language and its implementation. Addison-Wesley (1983).

[7]

C.A.R. Hoare, Communicating Sequential Processes. Prentice-Hall (1985).

[8]

S.N. Kamin and U.S. Reddy. Two semantic models of object-oriented languages. In C.A. Gunter and J.C. Mitchell (eds): Theoretical Aspects of Object-Oriented Programming, 463-495, MIT Press, (1994).

[9]

P.J. Landin, A correspondence between ALGOL 60 and Church's lambda-notation Part 1. Communications ACM 8.2 (1965) 89-101.

[10]

B. Meyer. Object-oriented Software Construction, Prentice-Hall second edition (1997).

[11]

R. Milner. Communication and Concurrency, Prentice Hall (1987).

[12]

B. Möller, Towards pointer algebra. Science of Computer Programming 21 (1993), 57-90.

[13]

B. Möller, Calculating with pointer structures. Proceedings of Mathematics for Software Construction, Chapman and Hall (1997), 24-48.

[14]

J.M. Morris, A general axiom of assignment, Assignment and linked data structure, A proof of the Schorr-Waite algorithm. In M Broy and G. Schmidt (eds.) Theoretical Foundations of Programming Methodology, 25-51, Reidel 1982 (Proceedings of the 1981 Marktoberdorf Summer School).

[15]

G. Nelson, Verifying reachability invariants of linked structures. Proceedings of POPL (1983), ACM Press, 38-47.

[16]

N. Suzuki, Analysis of pointer rotation. Communications ACM vol 25 No 5, May (1982), 330-335.

Cited By

Zhao LWang SLiu Z(2013)Graph-based object-oriented hoare logicTheories of Programming and Formal Methods10.5555/2554641.2554664(374-393)Online publication date: 1-Jan-2013
https://dl.acm.org/doi/10.5555/2554641.2554664
Ishtiaq SO'Hearn P(2011)BI as an assertion language for mutable data structuresACM SIGPLAN Notices10.1145/1988042.198805046:4(84-96)Online publication date: 20-May-2011
https://dl.acm.org/doi/10.1145/1988042.1988050
Tamalet AMadlener K(2010)Reasoning about assignments in recursive data structuresProceedings of the 13th Brazilian conference on Formal methods: foundations and applications10.5555/1987100.1987111(161-176)Online publication date: 8-Nov-2010
https://dl.acm.org/doi/10.5555/1987100.1987111
Show More Cited By

A Trace Model for Pointers and Objects
1. Theory of computation

Recommendations

A trace model for pointers and objects
Programming methodology

Object-oriented programs [5, 6, 10] are notoriously prone to the following kinds of error, which could lead to increasingly severe problems in the presence of tasking: 1. Following a null pointer; 2. Deletion of an accessible object; 3. Failure to ...
Analyses of pointers, induction variables, and container objects for dependence testing
Symbolic range analysis of pointers
CGO '16: Proceedings of the 2016 International Symposium on Code Generation and Optimization

Alias analysis is one of the most fundamental techniques that compilers use to optimize languages with pointers. However, in spite of all the attention that this topic has received, the current state-of-the-art approaches inside compilers still face ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

ECOOP '99: Proceedings of the 13th European Conference on Object-Oriented Programming

June 1999

528 pages

ISBN:3540661565

Editor:
Rachid Guerraoui

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 14 June 1999

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

16
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 04 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Zhao LWang SLiu Z(2013)Graph-based object-oriented hoare logicTheories of Programming and Formal Methods10.5555/2554641.2554664(374-393)Online publication date: 1-Jan-2013
https://dl.acm.org/doi/10.5555/2554641.2554664
Ishtiaq SO'Hearn P(2011)BI as an assertion language for mutable data structuresACM SIGPLAN Notices10.1145/1988042.198805046:4(84-96)Online publication date: 20-May-2011
https://dl.acm.org/doi/10.1145/1988042.1988050
Tamalet AMadlener K(2010)Reasoning about assignments in recursive data structuresProceedings of the 13th Brazilian conference on Formal methods: foundations and applications10.5555/1987100.1987111(161-176)Online publication date: 8-Nov-2010
https://dl.acm.org/doi/10.5555/1987100.1987111
Chen YSanders J(2010)Abstraction of object graphs in program verificationProceedings of the 10th international conference on Mathematics of program construction10.5555/1886619.1886628(80-99)Online publication date: 21-Jun-2010
https://dl.acm.org/doi/10.5555/1886619.1886628
Smith MGibbons J(2008)Unifying theories of locationsProceedings of the 2nd international conference on Unifying theories of programming10.5555/1893459.1893469(161-180)Online publication date: 8-Sep-2008
https://dl.acm.org/doi/10.5555/1893459.1893469
Smith MGibbons J(2007)Unifying theories of objectsProceedings of the 6th international conference on Integrated formal methods10.5555/1770498.1770529(599-618)Online publication date: 2-Jul-2007
https://dl.acm.org/doi/10.5555/1770498.1770529
Chen YSanders J(2006)Compositional reasoning for pointer structuresProceedings of the 8th international conference on Mathematics of Program Construction10.1007/11783596_10(115-139)Online publication date: 3-Jul-2006
https://dl.acm.org/doi/10.1007/11783596_10
Hoare T(2003)The verifying compilerProceedings of the 12th international conference on Compiler construction10.5555/1765931.1765957(262-272)Online publication date: 7-Apr-2003
https://dl.acm.org/doi/10.5555/1765931.1765957
Kubica M(2003)A temporal approach to specification and verification of pointer data-structuresProceedings of the 6th international conference on Fundamental approaches to software engineering10.5555/1762980.1763004(231-245)Online publication date: 7-Apr-2003
https://dl.acm.org/doi/10.5555/1762980.1763004
Meyer B(2003)Towards practical proofs of class correctnessProceedings of the 3rd international conference on Formal specification and development in Z and B10.5555/1761968.1761990(359-387)Online publication date: 4-Jun-2003
https://dl.acm.org/doi/10.5555/1761968.1761990
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents