We propose an approach for modular verification of programs written in an object-oriented language where, like in C++, the same virtual method call is bound to different methods at different points during the construction or destruction of an object. Our separation logic combines Parkinson and Bierman's abstract predicate families with essentially explicitly tracking each subobject's vtable pointer. Our logic supports polymorphic destruction. Virtual inheritance is not yet supported. We formalised our approach and implemented it in our VeriFast tool for semi-automated modular formal verification of C++ programs.

翻译：我们提出了一种对面向对象语言编写的程序进行模块化验证的方法，该方法中，与C++类似，同一虚方法调用在对象的构造或析构过程中的不同时间点会绑定到不同的方法。我们的分离逻辑将Parkinson和Bierman的抽象谓词族与显式追踪每个子对象的虚表指针相结合。该逻辑支持多态销毁，但尚未支持虚继承。我们将该方案形式化，并在我们的VeriFast工具中实现了对C++程序的半自动模块化形式化验证。