Reversible Debugging in Logic Programming

TL;DR

This paper introduces a reversible debugging scheme for logic programming, enabling developers to trace errors backwards through computations, with an implementation for Prolog called rever.

Contribution

It presents a novel reversible debugging approach for logic programs using Landauer embedding, and provides a practical implementation for Prolog.

Findings

Reversible debugging allows backward exploration of logic program execution.

The proposed Landauer embedding makes SLD resolution reversible.

The rever debugger for Prolog is publicly available.

Abstract

Reversible debugging is becoming increasingly popular for locating the source of errors. This technique proposes a more natural approach to debugging, where one can explore a computation from the observable misbehaviour backwards to the source of the error. In this work, we propose a reversible debugging scheme for logic programs. For this purpose, we define an appropriate instrumented semantics (a so-called Landauer embedding) that makes SLD resolution reversible. An implementation of a reversible debugger for Prolog, rever, has been developed and is publicly available.