Debugging the lists specification

We show here how to debug this lists specification. Recall we generated some test cases for this specification with

Maude> (test in REV_LIST : test .)

1 test cases were generated.

1 test cases have to be checked by the user:

	1. The term test(nil,0) has been reduced to false

This term can be straightforwardly debugged with

Maude> (invoke debugger with user test case 1 .)

Declarative debugging of wrong answers started.

Is this reduction (associated with the equation rev2) correct?

reverse(0) -> 0 0

Maude> (no .)

This reduction is incorrect, since we expected reverse(0) to be reduced to 0. The next question is:

Is this reduction (associated with the equation rev1) correct?

reverse(nil) -> 0

Maude> (no .)

This reduction is also wrong, because reverse(nil) should be nil. With these answers the debugger finds the following bug:

The buggy node is:
reverse(nil) -> 0
with the associated equation: rev1

In fact, if we check the specification, we notice that the user wrote the equation:

eq [rev1] : reverse(nil) = 0 .

that should be:

eq [rev1] : reverse(nil) = nil .