An abstract interpretation framework for refactoring with application to extract methods with contracts

ABSTRACT

Method extraction is a common refactoring feature provided by most modern IDEs. It replaces a user-selected piece of code with a call to an automatically generated method. We address the problem of automatically inferring contracts (precondition, postcondition) for the extracted method. We require the inferred contract: (a) to be valid for the extracted method (validity); (b) to guard the language and programmer assertions in the body of the extracted method by an opportune precondition (safety); (c) to preserve the proof of correctness of the original code when analyzing the new method separately (completeness); and (d) to be the most general possible (generality). These requirements rule out trivial solutions (e.g., inlining, projection, etc). We propose two theoretical solutions to the problem. The first one is simple and optimal. It is valid, safe, complete and general but unfortunately not effectively computable (except for unrealistic finiteness/decidability hypotheses). The second one is based on an iterative forward/backward method. We show it to be valid, safe, and, under reasonable assumptions, complete and general. We prove that the second solution subsumes the first. All justifications are provided with respect to a new, set-theoretic version of Hoare logic (hence without logic), and abstractions of Hoare logic, revisited to avoid surprisingly unsound inference rules.

We have implemented the new algorithms on the top of two industrial-strength tools (CCCheck and the Microsoft Roslyn CTP). Our experience shows that the analysis is both fast enough to be used in an interactive environment and precise enough to generate good annotations.

References

1. J. Arsac. Syntactic source to source transforms and program manipulation. Comm. ACM, 22 (1): 43--54, 1979.
2. A. Banerjee, D. A. Naumann, and S. Rosenberg. Regional logic for local reasoning about global invariants. In ECOOP, pp. 387--411, 2008.
3. F. Bannwart and P. Müller. Changing programs correctly: Refactoring with specifications. In FM 2006, volume 4085 of LNCS, pp. 492--507, 2006.
4. M. Barnett, M. Fahndrich, and F. Logozzo. Embedded contract languages. In SAC'10, pp. 2103--2110. ACM, 2010.
5. D. Beyer, T. A. Henzinger, R. Majumdar, and A. Rybalchenko. Path invariants. In phPLDI, pp. 300--309, 2007.
6. S. Brookes. A semantics for concurrent separation logic. Theor. Comput. Sci., 375 (1--3): 227--270, 2007.
7. L. Burdy, Y. Cheon, D. R. Cok, M. D. Ernst, J. R. Kiniry, G. T. Leavens, K. R. M. Leino, and E. Poll. An overview of JML tools and applications. STTT, 7 (3): 212--232, 2005.
8. P. Cousot. Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique de programmes (in French). Thése d'Étatés sciences mathématiques, Université scientifique et médicale de Grenoble, 1978.
9. P. Cousot. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. TCS, 277 (1--2): 47--103, 2002.
10. P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In Proc. Second Int. Symp. on Programming, pp. 106--130. Dunod, Paris, France, 1976.
11. P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, pp. 238--252, 1977.
12. P. Cousot and R. Cousot. Static determination of dynamic properties of recursive procedures. In E. Neuhold, editor, IFIP Conf. on Formal Description of Programming Concepts, pp. 237--277. North-Holland, 1977.
13. P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In POPL, pp. 269--282, 1979.
14. P. Cousot and R. Cousot. Constructive versions of Tarski's fixed point theorems. Pacific J. Math., 82 (1): 43--57, 1979.
15. P. Cousot and R. Cousot. Systematic design of program transformation frameworks by abstract interpretation. In POPL, pp. 178--190, 2002.
16. P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In POPL, pp. 84--97, 1978.
17. P. Cousot, R. Cousot, and L.Mauborgne. The reduced product of abstract domains and the combination of decision procedures. In FOSSACS, pp. 456--472, 2011.
18. P. Cousot, R. Cousot, and F. Logozzo. Contract precondition inference from intermittent assertions on collections. In VMCAI, pp. 150--168, 2011.
19. E. W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. CACM, 18 (8): 453--457, 1975.
20. M. Fahndrich and F. Logozzo. Static contract checking with abstract interpretation. In FoVeOOS, pp. 10--30, 2010.
21. A. Feldthaus, T. D. Millstein, A. Møller, M. Schafer, and F. Tip. Tool-supported refactoring for JavaScript. In OOPSLA, pp. 119--138, 2011.
22. J.-C. Filliâtre and M. Marché. The Why/Krakatoa/Caduceus platform for deductive program verification. In CAV, pp. 173--177, 2007.
23. C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for Java. In PLDI, pp. 234--245, 2002.
24. M. Fowler, K. Beck, J. Brant, W. Opdyke, and D. Roberts. Refactoring: Improving the Design of Existing Code. Addison-Wesley Professional, 1999.
25. A. Garrido and J. Meseguer. Formal specification and verification of Java refactorings. Technical Report UIUCDCS-R-2006--2731, Univ. of Illinois at Urbana-Champaign, 2006.
26. M. Goldstein, Y. Feldman, and S. Tyszberowicz. Refactoring with contracts. In AGILE, pp. 53--64. IEEE Computer Society, 2006.
27. A. Gotsman, J. Berdine, and B. Cook. Precision and the conjunction rule in concurrent separation logic. Electr. Notes Theor. Comput. Sci., 276: 171--190, 2011.
28. N. Halbwachs and M. Péron. Discovering properties about arrays in simple programs. In PLDI, pp. 339--348, 2008.
29. C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12 (10): 576--580, 1969.
30. V. Laviron and F. Logozzo. Subpolyhedra: a family of numerical abstract domains for the (more) scalable inference of linear inequalities. STTT, 13 (6): 585--601, 2011.
31. Q. Long, J. He, and Z. Liu. Refactoring and pattern-directed refactoring: A formal perspective. UNU-IIST Research Report 318, The United Nations Univ., 2005.
32. D. Loveman. Program improvement by source-to-source transformation. Journal of the ACM, 24 (1): 121--145, 1977.
33. K. L. McMillan. Relevance heuristics for program analysis. In POPL, pp. 145--146, 2008.
34. T. Mens and T. Tourwé. A survey of software refactoring. IEEE Trans. Software Eng., 30 (2): 126--139, 2004.
35. B. Meyer. Eiffel: The Language. Prentice Hall, 1991.
36. A. Miné. The octagon abstract domain. Higher-Order and Symbolic Computation, 19: 31--100, 2006.
37. K. Ng, M. Warren, P. Golde, and A. Hejlsberg. The Roslyn Project, Exposing the C# and VB compiler's code analysis. http://msdn.microsoft.com/en-us/roslyn, 2011.
38. P. W. O'Hearn. Resources, concurrency, and local reasoning. Theor. Comput. Sci., 375 (1--3): 271--307, 2007.
39. P. W. O'Hearn, H. Yang, and J. C. Reynolds. Separation and information hiding. In POPL, pp. 268--280, 2004.
40. S. Sankaranarayanan, F. Ivancic, and A. Gupta. Program analysis using symbolic ranges. In SAS, pp. 366--383, 2007.
41. T. Standish, D. Kibler, and J. Neighbors. Improving and refining programs by program manipulation. In ACMNC, pp. 509--516, 1976.
42. F. Tip. Refactoring using type constraints. In SAS, pp. 1--17, 2007.
43. W. Wake. Refactoring Workbook. Addison-Wesley, 2003.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Reliability

    • Validation

• Software and its engineering

  • Software creation and management

    • Software development process management

      • Software development methods

    • Software development techniques

    • Software verification and validation

      • Empirical software validation

      • Formal software verification

      • Process validation

  • Software notations and tools

    • System description languages

      • Specification languages

  • Software organization and properties

    • Extra-functional properties

      • Software reliability

    • Software functional properties

      • Correctness

      • Formal methods

• Theory of computation

  • Logic

    • Proof theory