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

Patrick Cousot, Radhia Cousot, Francesco Logozzo, Michael Barnett

Research output: Contribution to journalArticle

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.

Original languageEnglish (US)
Pages (from-to)213-232
Number of pages20
JournalACM SIGPLAN Notices
Volume47
Issue number10
DOIs
StatePublished - Oct 2012

Fingerprint

Computability and decidability

Keywords

  • Abstract interpretation
  • Design by contract
  • Method extraction
  • Program transformation
  • Refactoring
  • Static analysis

ASJC Scopus subject areas

  • Computer Science(all)

Cite this

An abstract interpretation framework for refactoring with application to extract methods with contracts. / Cousot, Patrick; Cousot, Radhia; Logozzo, Francesco; Barnett, Michael.

In: ACM SIGPLAN Notices, Vol. 47, No. 10, 10.2012, p. 213-232.

Research output: Contribution to journalArticle

Cousot, Patrick ; Cousot, Radhia ; Logozzo, Francesco ; Barnett, Michael. / An abstract interpretation framework for refactoring with application to extract methods with contracts. In: ACM SIGPLAN Notices. 2012 ; Vol. 47, No. 10. pp. 213-232.
@article{dffb4b77fd7e4e5295920399ca6ad747,
title = "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.",
keywords = "Abstract interpretation, Design by contract, Method extraction, Program transformation, Refactoring, Static analysis",
author = "Patrick Cousot and Radhia Cousot and Francesco Logozzo and Michael Barnett",
year = "2012",
month = "10",
doi = "10.1145/2398857.2384633",
language = "English (US)",
volume = "47",
pages = "213--232",
journal = "ACM SIGPLAN Notices",
issn = "1523-2867",
publisher = "Association for Computing Machinery (ACM)",
number = "10",

}

TY - JOUR

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

AU - Cousot, Patrick

AU - Cousot, Radhia

AU - Logozzo, Francesco

AU - Barnett, Michael

PY - 2012/10

Y1 - 2012/10

N2 - 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.

AB - 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.

KW - Abstract interpretation

KW - Design by contract

KW - Method extraction

KW - Program transformation

KW - Refactoring

KW - Static analysis

UR - http://www.scopus.com/inward/record.url?scp=84870422038&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84870422038&partnerID=8YFLogxK

U2 - 10.1145/2398857.2384633

DO - 10.1145/2398857.2384633

M3 - Article

VL - 47

SP - 213

EP - 232

JO - ACM SIGPLAN Notices

JF - ACM SIGPLAN Notices

SN - 1523-2867

IS - 10

ER -