Sultana, Nik and Thompson, Simon (2008) Mechanical Verification of Refactorings. In: PEPM '08 Proceedings of the 2008 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation. PEPM Partial Evaluation and Program Manipulation . ACM, New York, USA, pp. 51-60. ISBN 978-1-59593-977-7. (doi:10.1145/1328408.1328417) (KAR id:23959)
PDF
Language: English |
|
Download this file (PDF/233kB) |
![]() |
Request a format suitable for use with assistive technology e.g. a screenreader | |
Official URL: http://dx.doi.org/10.1145/1328408.1328417 |
Abstract
In this paper we describe the formal verification of refactorings for untyped and typed lambda-calculi. This verification is performed in the proof assistant Isabelle/HOL. Refactorings are program transformations applied to improve the design of source code. Well-structured source code is easier and cheaper to maintain, and this motivates the use of refactoring. These transformations have been implemented as programmer tools and, as with other metaprogramming tools, it is desirable that implementations of refactorings are correct. For a refactoring to be correct the refactored program must be identical in behaviour to the original program. Since refactorings are source-to-source transformations, concrete program information matters: for example, names (of variables, procedures, etc) and program layout should also be preserved by refactoring. This is a particular characteristic of refactorings since general program transformations operate over machine representations of programs, rather than readable source code. The paper describes the formalisation adopted, and the alternatives explored. It also reflects on some of the difficulties of performing such formalisations, the interaction between refactoring and phases such as type-checking and parsing, and the generation of correct implementations from mechanised proofs.
Item Type: | Book section |
---|---|
DOI/Identification number: | 10.1145/1328408.1328417 |
Uncontrolled keywords: | Theory, Verification, Refactoring, Isabelle/HOL |
Subjects: | Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, |
Divisions: | Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing |
Funders: | Association for Computing Machinery (https://ror.org/03wsadn68) |
Depositing User: | Mark Wheadon |
Date Deposited: | 29 Mar 2010 12:09 UTC |
Last Modified: | 02 Jan 2024 23:08 UTC |
Resource URI: | https://kar.kent.ac.uk/id/eprint/23959 (The current URI for this page, for reference purposes) |
- Link to SensusAccess
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):