论文标题
使用Verifast验证C ++程序
Verification of C++ Programs with VeriFast
论文作者
论文摘要
Verifast是基于分离逻辑的原型工具，用于C和Java程序的模块化验证。我们正在添加对C ++的支持。在本报告中，我们描述了到目前为止我们添加支持的C ++功能，以及我们为这些功能生成的证明义务。 At this point, VeriFast has basic support for most object-oriented programming features of C++: member functions, member function and operator overloading, implicit and explicit conversions, constructors and initializer lists, destructors, reference types, allocation and deallocation on the stack or on the heap (using new and delete), inheritance (including multiple inheritance but not virtual base classes), and virtual member functions and overriding.为了支持继承层次结构的规范，我们为实例谓词增加了支持，可以在基类中引入并在派生类中覆盖。此时，主要缺少功能是支持C ++模板，我们计划下一步进行。
VeriFast is a prototype tool based on separation logic for modular verification of C and Java programs. We are in the process of adding support for C++. In this report, we describe the features of C++ for which we added support so far, as well as the proof obligations we generate for these features. At this point, VeriFast has basic support for most object-oriented programming features of C++: member functions, member function and operator overloading, implicit and explicit conversions, constructors and initializer lists, destructors, reference types, allocation and deallocation on the stack or on the heap (using new and delete), inheritance (including multiple inheritance but not virtual base classes), and virtual member functions and overriding. To support specification of inheritance hierarchies, we added support for instance predicates, which can be introduced in a base class and overridden in derived classes. The main missing feature at this point is support for C++ templates, which we plan to work on next.
