DDebugger

Declarative debugging of rewriting logic specifications. Declarative debugging is a semi-automatic technique that starts from an incorrect computation and locates a program fragment responsible for the error by building a tree representing this computation and guiding the user through it to find the error. Membership equational logic (MEL) is an equational logic that in addition to equations allows one to state membership axioms characterizing the elements of a sort. Rewriting logic is a logic of change that extends MEL by adding rewrite rules, which correspond to transitions between states and can be nondeterministic. We propose here a calculus to infer reductions, sort inferences, normal forms, and least sorts with the equational subset of rewriting logic, and rewrites and sets of reachable terms through rules. We use an abbreviation of the proof trees computed with this calculus to build appropriate debugging trees for both wrong (an incorrect result obtained from an initial result) and missing answers (results that are erroneous because they are incomplete), whose adequacy for debugging is proved. Using these trees we have implemented Maude DDebugger, a declarative debugger for Maude, a high-performance system based on rewriting logic. We illustrate its use with an example.


References in zbMATH (referenced in 15 articles )

Showing results 1 to 15 of 15.
Sorted by year (citations)

  1. Riesco, Adrián; Ogata, Kazuhiro; Futatsugi, Kokichi: A Maude environment for CafeOBJ (2017)
  2. Alpuente, María; Ballis, Demis; Frechina, Francisco; Sapiña, Julia: Debugging Maude programs via runtime assertion checking and trace slicing (2016)
  3. Alpuente, M.; Ballis, D.; Frechina, F.; Sapiña, J.: Exploring conditional rewriting logic computations (2015)
  4. Alpuente, María; Ballis, Demis; Frechina, Francisco; Sapiña, Julia: Inspecting rewriting logic computations (in a parametric and stepwise way) (2014)
  5. Insa, David; Silva, Josep; Tomás, César: Enhancing declarative debugging with loop expansion and tree compression (2013)
  6. Meseguer, José: Twenty years of rewriting logic (2012)
  7. Pita, Isabel; Riesco, Adrián: A tool for testing data type implementations from Maude algebraic specifications (2012) ioport
  8. Riesco, Adrián: Using narrowing to test Maude specifications (2012) ioport
  9. Riesco, Adrián: Using semantics specified in Maude to generate test cases (2012) ioport
  10. Riesco, Adrián: Test-case generation for Maude functional modules (2012) ioport
  11. Riesco, Adrián; Verdejo, Alberto; Martí-Oliet, Narciso; Caballero, Rafael: Declarative debugging of rewriting logic specifications (2012)
  12. Riesco, Adrián; Verdejo, Alberto; Martí-Oliet, Narciso: A complete declarative debugger for Maude (2011)
  13. Riesco, Adrian; Verdejo, Alberto; Martí-Oliet, Narciso: Enhancing the debugging of Maude specifications (2010)
  14. Riesco, Adrián; Verdejo, Alberto; Martí-Oliet, Narciso: Declarative debugging of missing answers for Maude (2010)
  15. Riesco, Adrian; Verdejo, Alberto; Caballero, Rafael; Martí-Oliet, Narciso: Declarative debugging of rewriting logic specifications (2009)