Automatic annotating and checking of dynamic ownership

作者：Hu Tingting^*; Liu Haiyang; Zhang Ke; Qiu Zongyan

来源：20th Brazilian Symposium on Programming Languages, SBLP 2016, 2016-09-22 to 2016-09-23.

DOI：10.1007/978-3-319-45279-1_6

• Aliasing
• Object ownership
• Program analysis
• Program Verification
• Topology error

Object ownership is an important technique in dealing with object sharing and aliasing to support verification of OO programs. Dynamic Ownership proposes a very flexible encapsulation discipline and has been adopted in Spec#. However, to use this technique, programmers have to keep all the ownership information in mind to decide the validation for modifying one variable. This makes the approach difficult to master and use. In this paper, we apply data-flow analysis to generate most annotations of dynamic ownership automatically, thus can potentially reduce the workload of program verification. Moreover, our technique can reveal ownership topology errors and encapsulation errors. In addition, the entire analysis of our approach is static, thus is efficient.

• 出版日期2016
• 单位北京大学