We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: PEQcheck: Localized and Context-aware Checking of Functional Equivalence (Technical Report)

Abstract: Refactorings must not alter the program's functionality. However, not all refactorings fulfill this requirement. Hence, one must explicitly check that a refactoring does not alter the functionality. Since one rarely has a formal specification of the program's behavior, we utilize the original program as functional specification. Then, we check whether the original and refactored program are functionally equivalent. To this end, we apply a common idea and reduce equivalence checking to program verification. To increase efficiency, our equivalence checker PEQcheck constructs one verification task per refactored code segment instead of one per function as typically done by prior work. In addition, PEQcheck considers the context of the code segments. For instance, only variables that are modified and live are required to be equivalent and read-only variables may be shared between original and refactored code segments. We show that PEQcheck is sound.Moreover, our evaluation testifies that the localized and context-aware checking performed by \peqcheck can indeed be beneficial.
Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)
Cite as: arXiv:2101.09042 [cs.LO]
  (or arXiv:2101.09042v2 [cs.LO] for this version)

Submission history

From: Marie-Christine Jakobs [view email]
[v1] Fri, 22 Jan 2021 10:29:41 GMT (55kb)
[v2] Mon, 22 Mar 2021 21:22:55 GMT (56kb)

Link back to: arXiv, form interface, contact.