Patrick Cousot, Radhia Cousot, Francesco Logozzo, & Michael Barnett.<bR> An abstract interpretation framework for refactoring with application to extract methods with contracts.

Patrick Cousot, Radhia Cousot, Francesco Logozzo, and Michael Barnett.
An abstract interpretation framework for refactoring with application to extract methods with contracts.
In Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2012, part of SPLASH 2012, Tucson, AZ, USA, October 21—25, 2012, pp. 213—232, 2012. © ACM Press, New York.
Letter paper format: Paper (PDF 2.4 Mb)
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 (pre- condition, 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.
Categories and Subject Descriptors: D.1.0 [Programming Techniques/General];
D.2.1 [Programming Techniques/Requirements/Specifications];
D.2.2 [Programming Techniques/Design Tools and Technique];
D.2.4 [Programming Techniques/Software/Program Verification];
D.2.4 [Programming Techniques/Software/Testing and Debugging].
General Terms: Design, Documentation, Experimentation, Human Factors, Languages, Reliability, Verification.
Keywords: Abstract interpretation, Design by contract, Method extraction, Program transformation, Refactoring, Static analysis.
Slides of the 25mn OOPSLA'12 presentation by Francesco Logozzo are available in US Letter 4 slides/page PDF (15 Mb)

Bibliographic reference:

\bibitem{CousotCousotLogozzoBarnett-OOPSLA12}
P.~Cousot, R.~Cousot, F.~Logozzo, \& M.~Barnett.
\newblock An abstract interpretation framework for refactoring with
          application to extract methods with contracts.
\newblock In \emph{Proceedings of the 27th Annual ACM SIGPLAN Conference 
          on Object-Oriented Programming, Systems, Languages, and Applications,
          OOPSLA 2012}, pages 213--232, Tucson, AZ, USA, October 21--25, 2012. 
          ACM Press, New York, NY.

@inproceedings{CousotCousotLogozzoBarnett-OOPSLA12,
  author    = {Patrick Cousot and
               Radhia Cousot and
               Francesco Logozzo and
               Michael Barnett},
  title     = {An abstract interpretation framework for refactoring with
               application to extract methods with contracts},
  booktitle = {Proceedings of the 27th Annual ACM SIGPLAN Conference on
               Object-Oriented Programming, Systems, Languages, and Applications,
               OOPSLA 2012, part of SPLASH 2012, Tucson, AZ, USA, October
               21--25, 2012},
  editor    = {Gary T. Leavens and
               Matthew B. Dwyer},
  publisher = {ACM},
  year      = {2012},
  pages     = {213--232},
  isbn      = {978-1-4503-1561-6},
  ee        = {http://doi.acm.org/10.1145/2384616.2384633},
}

Copyright: © ACM, (2014). This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in the Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2012, part of SPLASH 2012, Tucson, AZ, USA, October 21—25, 2012 © 2012 ACM

copyright notice, ACM copyright
Last modified: Tue May 13 09:33:07 EDT 2014