External Behavior of a Logic Program and Verification of Refactoring

TL;DR

This paper defines the external behavior of a logic program in a simple answer set programming language and introduces a proof assistant to verify correct refactoring without altering that behavior.

Contribution

It formalizes external behavior in a logic programming context and provides a tool for verifying refactoring correctness.

Findings

Formal definition of external behavior for the language

Development of a proof assistant for verification

Ensures refactoring preserves program behavior

Abstract

Refactoring is modifying a program without changing its external behavior. In this paper, we make the concept of external behavior precise for a simple answer set programming language. Then we describe a proof assistant for the task of verifying that refactoring a program in that language is performed correctly.