Simplifying questions in Maude declarative debugger by transforming proof trees

In G. Vidal, editor, Logic-Based Program Synthesis and Transformation - 21st International Symposium, LOPSTR 2011, LNCS 7225, pages 73-89. Springer, 2012. © Springer-Verlag

Abstract: Declarative debugging is a debugging technique that abstracts the execution details that in general may be difficult to follow in declarative languages to focus on results. It relies on a data structure representing the wrong computation, the debugging tree, which is traversed by asking questions to the user about the correctness of the computation steps related to each node. Thus, the complexity of the questions is an important factor regarding the applicability of the technique. In this paper we present a transformation for debugging trees for Maude specifications that ensures that any subterm occurring in a question has been previously replaced by the most reduced form that it has taken during the computation, thus ensuring that questions become as simple as possible.

[pdf]

@inproceedings{lopstr/CaballeroRVM11,
  author    = {Rafael Caballero and
               Adri{\'a}n Riesco and
               Alberto Verdejo and
               Narciso Mart\'{\i}-Oliet},
  title     = {Simplifying Questions in {Maude} Declarative Debugger by Transforming
               Proof Trees},
  year      = {2011},
  pages     = {73-89},
  url        = {http://dx.doi.org/10.1007/978-3-642-32211-2_6},
  editor    = {Germ{\'a}n Vidal},
  booktitle     = {Logic-Based Program Synthesis and Transformation - 21st
               International Symposium, LOPSTR 2011, Odense, Denmark, July
               18-20, 2011. Revised Selected Papers},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {7225}
}