Automatic Annotating And Checking Of Dynamic Ownership

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.