Formal treatment of RAII and/or safe deallocations in C++

Are there any research papers on formal treatment of RAII and/or 开发者_运维百科safe deallocations in C++?

---

Take a look at "A Mechanized Semantics for C++ Object Construction and Destruction, with Applications to Resource Management" (page, different PDF version), which has apparently been submitted to POPL 2012; but AFAIK has not yet been peer reviewed.

There is a section specifically on RAII, although it may not prove what you want:

We cannot prove a general result guaranteeing the proper encapsulation of resources in classes: this is a matter of program verification. We can, however, prove that in a terminating program every construction of a subobject is correctly matched by a destruction.

Disclaimer: I've only briefly skimmed the paper, and I know almost nothing about formal language semantics.