research-article

A mechanized semantics for C++ object construction and destruction, with applications to resource management

Authors:

Tahina Ramananandro,

Gabriel Dos Reis,

Xavier LeroyAuthors Info & Claims

POPL '12: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 521 - 532

https://doi.org/10.1145/2103656.2103718

Published: 25 January 2012 Publication History

Abstract

We present a formal operational semantics and its Coq mechanization for the C++ object model, featuring object construction and destruction, shared and repeated multiple inheritance, and virtual function call dispatch. These are key C++ language features for high-level system programming, in particular for predictable and reliable resource management. This paper is the first to present a formal mechanized account of the metatheory of construction and destruction in C++, and applications to popular programming techniques such as "resource acquisition is initialization". We also report on irregularities and apparent contradictions in the ISO C++03 and C++11 standards.

Supplementary Material

JPG File (popl_8a_2.jpg)

Download
9.35 KB

MP4 File (popl_8a_2.mp4)

Download
200.59 MB

References

[1]

The Coq proof assistant, 1999--2012. URL http://coq.inria.fr.

[2]

M. A. Ellis and B. Stroustrup. The Annotated C++ Reference Manual. Addison-Wesley, 1990.

Digital Library

[3]

M. Fahndrich and S. Xia. Establishing object invariants with delayed types. In 22nd conf. on Object-Oriented Programming Systems and Applications (OOPSLA'07), pages 337--350. ACM, 2007.

Digital Library

[4]

J. Gosling, B. Joy, G. Steele, and G. Bracha. The Java Language Specification. Addison Wesley, 3rd edition edition, 2005.

Digital Library

[5]

L. Hubert, T. Jensen, V. Monfort, and D. Pichardie. Enforcing secure object initialization in Java. In Computer Security -- ESORICS 2010, volume 6345 of Lecture Notes in Computer Science, pages 101--115. Springer, 2010.

Digital Library

[6]

International Standard ISO/IEC 14882:2003. Programming Languages -- C++. International Organization for Standards, 2003.

[7]

International Standard ISO/IEC 14882:2011. Programming Languages -- C++. International Organization for Standards, 2011.

[8]

X. Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 43 (4): 363--446, 2009.

Digital Library

[9]

Lockheed Martin. Joint Strike Fighter Air Vehicle C+ Coding Standards for the System Development and Demonstration Program, 2005. URL http://www.research.att.com/ bs/JSF-AV-rules.pdf.

[10]

M. Norrish. A formal semantics for C+. Technical report, NICTA, 2008.

[11]

X. Qi and A. C. Myers. Masked types for sound object initialization. In 36th symp. Principles of Programming Languages (POPL'09), pages 53--65. ACM, 2009.

Digital Library

[12]

T. Ramananandro. phMechanized Formal Semantics and Verified Compilation for C+ Objects. PhD thesis, Université Paris Diderot, Jan. 2012.

[13]

T. Ramananandro, G. Dos Reis, and X. Leroy. Formal verification of object layout for C+ multiple inheritance. In 38th symp. Principles of Programming Languages (POPL'11), pages 67--80. ACM, 2011.

Digital Library

[14]

J. G. Rossie and D. P. Friedman. An algebraic semantics of subobjects. In 10th conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'95), pages 187--199. ACM, 1995.

Digital Library

[15]

B. Stroustrup. Classes: An abstract data type facility for the C language. SIGPLAN Not., 17: 42--51, January 1982.

Digital Library

[16]

B. Stroustrup. phThe design and evolution of C+. ACM Press/Addison-Wesley Publishing Co., New York, NY, USA, 1994.

Digital Library

[17]

D. Wasserrab. phFrom Formal Semantics to Verified Slicing -- A Modular Framework with Applications in Language Based Security. PhD thesis, Karlsruher Institut für Technologie, Fakultat für Informatik, Oct. 2010.

[18]

D. Wasserrab, T. Nipkow, G. Snelting, and F. Tip. An operational semantics and type safety proof for multiple inheritance in C+. In ph21st conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'06), pages 345--362. ACM, 2006.

Digital Library

Cited By

Park JYoun DLee KRyu S(2023)Feature-Sensitive Coverage for Conformance Testing of Programming Language ImplementationsProceedings of the ACM on Programming Languages10.1145/35912407:PLDI(493-515)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591240
Martin-Martin EMontenegro MRiesco ARodríguez-Hortalá JRubio R(2023)Verification of the ROS NavFn planner using executable specification languagesJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2023.100860132(100860)Online publication date: Apr-2023
https://doi.org/10.1016/j.jlamp.2023.100860
Xu HChen ZSun MZhou YLyu M(2021)Memory-Safety Challenge Considered Solved? An In-Depth Study with All Rust CVEsACM Transactions on Software Engineering and Methodology10.1145/346664231:1(1-25)Online publication date: 28-Sep-2021
https://dl.acm.org/doi/10.1145/3466642
Show More Cited By

Index Terms

A mechanized semantics for C++ object construction and destruction, with applications to resource management

Recommendations

A mechanized semantics for C++ object construction and destruction, with applications to resource management
POPL '12

We present a formal operational semantics and its Coq mechanization for the C++ object model, featuring object construction and destruction, shared and repeated multiple inheritance, and virtual function call dispatch. These are key C++ language ...
What Is Object-Oriented Programming?

The meaning of the term 'object oriented' is examined in the context of the general-purpose programming language C++. This choice is made partly to introduce C++ and partly because C++ is one of the few languages that supports data abstraction, object-...
A pragmatic approach to C++, Eiffel and Ada 9X programming

Conceptualizing the world as a set of interacting objects, has ever been the main mechanism of perception associated with humankind. Therefore, the formulation of languages and modeling and design methods based on object orientation (OO) was just a ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '12: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2012

602 pages

ISBN:9781450310833

DOI:10.1145/2103656

General Chair:
John Field
Google, USA
,
Program Chair:
Michael Hicks
University of Maryland, College Park, USA

ACM SIGPLAN Notices Volume 47, Issue 1
POPL '12
January 2012
569 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2103621
Issue’s Table of Contents

Copyright © 2012 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]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 January 2012

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL '12

Sponsor:

SIGPLAN

POPL '12: The 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 25 - 27, 2012

PA, Philadelphia, USA

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
473
Total Downloads

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

Reflects downloads up to 26 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Park JYoun DLee KRyu S(2023)Feature-Sensitive Coverage for Conformance Testing of Programming Language ImplementationsProceedings of the ACM on Programming Languages10.1145/35912407:PLDI(493-515)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591240
Martin-Martin EMontenegro MRiesco ARodríguez-Hortalá JRubio R(2023)Verification of the ROS NavFn planner using executable specification languagesJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2023.100860132(100860)Online publication date: Apr-2023
https://doi.org/10.1016/j.jlamp.2023.100860
Xu HChen ZSun MZhou YLyu M(2021)Memory-Safety Challenge Considered Solved? An In-Depth Study with All Rust CVEsACM Transactions on Software Engineering and Methodology10.1145/346664231:1(1-25)Online publication date: 28-Sep-2021
https://dl.acm.org/doi/10.1145/3466642
Stroustrup B(2020)Thriving in a crowded and changing world: C++ 2006–2020Proceedings of the ACM on Programming Languages10.1145/33863204:HOPL(1-168)Online publication date: 12-Jun-2020
https://dl.acm.org/doi/10.1145/3386320
Becker HCrespo JGalowicz JHensel UHirai YKunz CNakata KSacchini JTews HTuerk T(2016)Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a HypervisorFM 2016: Formal Methods10.1007/978-3-319-48989-6_5(69-84)Online publication date: 8-Nov-2016
https://doi.org/10.1007/978-3-319-48989-6_5
Xiao XBalakrishnan GIvančić FMaeda NGupta AChhetri DPăsăreanu CMarinov D(2014)ARC++: effective typestate and lifetime dependency analysisProceedings of the 2014 International Symposium on Software Testing and Analysis10.1145/2610384.2610395(116-126)Online publication date: 21-Jul-2014
https://dl.acm.org/doi/10.1145/2610384.2610395
Stroustrup B(2012)Foundations of c++Proceedings of the 21st European conference on Programming Languages and Systems10.1007/978-3-642-28869-2_1(1-25)Online publication date: 24-Mar-2012
https://dl.acm.org/doi/10.1007/978-3-642-28869-2_1
Cui MXu HTian HZhou Y(2024)rCanary: Detecting Memory Leaks Across Semi-Automated Memory Management Boundary in RustIEEE Transactions on Software Engineering10.1109/TSE.2024.344362450:9(2472-2484)Online publication date: 13-Aug-2024
https://dl.acm.org/doi/10.1109/TSE.2024.3443624
Cui MChen CXu HZhou Y(2023)SafeDrop: Detecting Memory Deallocation Bugs of Rust Programs via Static Data-flow AnalysisACM Transactions on Software Engineering and Methodology10.1145/354294832:4(1-21)Online publication date: 26-May-2023
https://dl.acm.org/doi/10.1145/3542948
He YWu WChen Y(2012)An efficient method for detecting concurrency errors in object-oriented programsScience China Information Sciences10.1007/s11432-012-4751-z55:12(2774-2784)Online publication date: 29-Dec-2012
https://doi.org/10.1007/s11432-012-4751-z

View Options

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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents