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.
Type de document :
Communication dans un congrès
POPL '12 - 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2012, Philadelphia, PA, United States. pp.521-532, 2012, <10.1145/2103656.2103718>
Liste complète des métadonnées

https://hal.inria.fr/hal-00674663
Contributeur : Xavier Leroy <>
Soumis le : lundi 27 février 2012 - 19:15:37
Dernière modification le : mercredi 28 mars 2012 - 13:25:34
Document(s) archivé(s) le : lundi 26 novembre 2012 - 10:17:00

Fichier

cpp-construction.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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, Jan 2012, Philadelphia, PA, United States. pp.521-532, 2012, <10.1145/2103656.2103718>. <hal-00674663>

Partager

Métriques

Consultations de
la notice

164

Téléchargements du document

118