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

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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/hal-00674663
Contributor : Xavier Leroy <>
Submitted on : Monday, February 27, 2012 - 7:15:37 PM
Last modification on : Friday, May 25, 2018 - 12:02:07 PM
Long-term archiving on : Monday, November 26, 2012 - 10:17:00 AM

File

cpp-construction.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Tahina Ramananandro, Gabriel dos Reis, Xavier Leroy. A mechanized semantics for C++ object construction and destruction, with applications to resource management. POPL '12 - 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM, Jan 2012, Philadelphia, PA, United States. pp.521-532, ⟨10.1145/2103656.2103718⟩. ⟨hal-00674663⟩

Share

Metrics

Record views

314

Files downloads

268