Towards specification-guarded refactoring

Adam David Barwell; Christopher Mark Brown; Susmit Sarkar

doi:10.1007/978-3-031-71294-4_9

Towards specification-guarded refactoring

Adam David Barwell, Christopher Mark Brown, Susmit Sarkar^*

^*Corresponding author for this work

School of Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

Refactoring is a common task in writing and maintaining software. Refactoring tools are available for a wide variety of programming languages, and they are intended to transform source code without altering the functional behaviour of the software being refactored. However, even though most refactoring tools are designed with this criterion in mind, and programmers expect it, their implementations do not provide formal guarantees of correctness. To address this limitation, we propose a methodology for extending refactoring implementations with correctness guarantees. Our approach leverages dependently-typed languages and techniques to guard refactoring implementations with proofs of conformance to formal specifications. We illustrate our proposed methodology using a renaming refactoring that includes correctness guarantees as an integral part of its implementation.

Original language	English
Title of host publication	Logic-based program synthesis and transformation
Subtitle of host publication	34th International symposium, LOPSTR 2024, Milan, Italy, September 9–10, 2024, Proceedings
Editors	Juliana Bowles, Harald Søndergaard
Place of Publication	Cham
Publisher	Springer
Pages	149–165
ISBN (Electronic)	9783031712944
ISBN (Print)	9783031712937
DOIs	https://doi.org/10.1007/978-3-031-71294-4_9
Publication status	Published - 7 Sept 2024

Publication series

Name	Lecture notes in computer science
Publisher	Springer Nature
Volume	14919
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Keywords

Haskell
Refactoring
Dependent types
Idris
Correctness
Soundness
Renaming
Equivalence
Semantics

Access to Document

10.1007/978-3-031-71294-4_9

Barwell-2024-Towards-specification-guarded-LOPSTR2024-AAM-CCBY
Copyright © 2024 the Authors. This work has been made available online in accordance with the University of St Andrews Open Access policy. This accepted manuscript is distributed under the terms of the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original author and source are credited. The final published version of this work is available at https://doi.org/10.1007/978-3-031-71294-4_9.
Accepted author manuscript, 490 KBLicence: CC BY

Energise: Refactorings and Skeletons for: Energise: Refactorings and Skeletons for Energy-Aware Applications on High-Performance Embedded Systems
Brown, C. M. (PI)
EPSRC
1/04/21 → 31/03/24
Project: Standard

Cite this

Barwell, A. D., Brown, C. M., & Sarkar, S. (2024). Towards specification-guarded refactoring. In J. Bowles, & H. Søndergaard (Eds.), Logic-based program synthesis and transformation: 34th International symposium, LOPSTR 2024, Milan, Italy, September 9–10, 2024, Proceedings (pp. 149–165). (Lecture notes in computer science; Vol. 14919). Springer. https://doi.org/10.1007/978-3-031-71294-4_9

Barwell, Adam David ; Brown, Christopher Mark ; Sarkar, Susmit. / Towards specification-guarded refactoring. Logic-based program synthesis and transformation: 34th International symposium, LOPSTR 2024, Milan, Italy, September 9–10, 2024, Proceedings. editor / Juliana Bowles ; Harald Søndergaard. Cham : Springer, 2024. pp. 149–165 (Lecture notes in computer science).

@inproceedings{0c4546e1eabb459f8df1ba371f6ebae3,

title = "Towards specification-guarded refactoring",

abstract = "Refactoring is a common task in writing and maintaining software. Refactoring tools are available for a wide variety of programming languages, and they are intended to transform source code without altering the functional behaviour of the software being refactored. However, even though most refactoring tools are designed with this criterion in mind, and programmers expect it, their implementations do not provide formal guarantees of correctness. To address this limitation, we propose a methodology for extending refactoring implementations with correctness guarantees. Our approach leverages dependently-typed languages and techniques to guard refactoring implementations with proofs of conformance to formal specifications. We illustrate our proposed methodology using a renaming refactoring that includes correctness guarantees as an integral part of its implementation.",

keywords = "Haskell, Refactoring, Dependent types, Idris, Correctness, Soundness, Renaming, Equivalence, Semantics",

author = "Barwell, {Adam David} and Brown, {Christopher Mark} and Susmit Sarkar",

note = "Funding: This work was generously supported by UK EPSRC, EP/V006290.",

year = "2024",

month = sep,

day = "7",

doi = "10.1007/978-3-031-71294-4_9",

language = "English",

isbn = "9783031712937",

series = "Lecture notes in computer science",

publisher = "Springer",

pages = "149–165",

editor = "Juliana Bowles and Harald S{\o}ndergaard",

booktitle = "Logic-based program synthesis and transformation",

address = "Netherlands",

}

Barwell, AD , Brown, CM & Sarkar, S 2024, Towards specification-guarded refactoring. in J Bowles & H Søndergaard (eds), Logic-based program synthesis and transformation: 34th International symposium, LOPSTR 2024, Milan, Italy, September 9–10, 2024, Proceedings. Lecture notes in computer science, vol. 14919, Springer, Cham, pp. 149–165. https://doi.org/10.1007/978-3-031-71294-4_9

Towards specification-guarded refactoring. / Barwell, Adam David ; Brown, Christopher Mark ; Sarkar, Susmit.
Logic-based program synthesis and transformation: 34th International symposium, LOPSTR 2024, Milan, Italy, September 9–10, 2024, Proceedings. ed. / Juliana Bowles; Harald Søndergaard. Cham: Springer, 2024. p. 149–165 (Lecture notes in computer science; Vol. 14919).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Towards specification-guarded refactoring

AU - Barwell, Adam David

AU - Brown, Christopher Mark

AU - Sarkar, Susmit

N1 - Funding: This work was generously supported by UK EPSRC, EP/V006290.

PY - 2024/9/7

Y1 - 2024/9/7

N2 - Refactoring is a common task in writing and maintaining software. Refactoring tools are available for a wide variety of programming languages, and they are intended to transform source code without altering the functional behaviour of the software being refactored. However, even though most refactoring tools are designed with this criterion in mind, and programmers expect it, their implementations do not provide formal guarantees of correctness. To address this limitation, we propose a methodology for extending refactoring implementations with correctness guarantees. Our approach leverages dependently-typed languages and techniques to guard refactoring implementations with proofs of conformance to formal specifications. We illustrate our proposed methodology using a renaming refactoring that includes correctness guarantees as an integral part of its implementation.

AB - Refactoring is a common task in writing and maintaining software. Refactoring tools are available for a wide variety of programming languages, and they are intended to transform source code without altering the functional behaviour of the software being refactored. However, even though most refactoring tools are designed with this criterion in mind, and programmers expect it, their implementations do not provide formal guarantees of correctness. To address this limitation, we propose a methodology for extending refactoring implementations with correctness guarantees. Our approach leverages dependently-typed languages and techniques to guard refactoring implementations with proofs of conformance to formal specifications. We illustrate our proposed methodology using a renaming refactoring that includes correctness guarantees as an integral part of its implementation.

KW - Haskell

KW - Refactoring

KW - Dependent types

KW - Idris

KW - Correctness

KW - Soundness

KW - Renaming

KW - Equivalence

KW - Semantics

U2 - 10.1007/978-3-031-71294-4_9

DO - 10.1007/978-3-031-71294-4_9

M3 - Conference contribution

SN - 9783031712937

T3 - Lecture notes in computer science

SP - 149

EP - 165

BT - Logic-based program synthesis and transformation

A2 - Bowles, Juliana

A2 - Søndergaard, Harald

PB - Springer

CY - Cham

ER -

Barwell AD , Brown CM , Sarkar S. Towards specification-guarded refactoring. In Bowles J, Søndergaard H, editors, Logic-based program synthesis and transformation: 34th International symposium, LOPSTR 2024, Milan, Italy, September 9–10, 2024, Proceedings. Cham: Springer. 2024. p. 149–165. (Lecture notes in computer science). Epub 2024 Sept 6. doi: 10.1007/978-3-031-71294-4_9

Towards specification-guarded refactoring

Abstract

Publication series

Keywords

Access to Document

Fingerprint

Projects

Energise: Refactorings and Skeletons for: Energise: Refactorings and Skeletons for Energy-Aware Applications on High-Performance Embedded Systems

Cite this