Sciweavers

Share
POPL
2012
ACM

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

8 years 11 months ago
A mechanized semantics for C++ object construction and destruction, with applications to resource management
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.
Tahina Ramananandro, Gabriel Dos Reis, Xavier Lero
Added 25 Apr 2012
Updated 25 Apr 2012
Type Journal
Year 2012
Where POPL
Authors Tahina Ramananandro, Gabriel Dos Reis, Xavier Leroy
Comments (0)
books