*************************************************************************
DECLARATIVE DEBUGGER FOR FUNCTIONAL LOGIC PROGRAMS .
*************************************************************************
*************************************************************************
*** help. -> display menu ***
*** clean. -> clean program and specification ***
*** loadprg. -> read in program to be corrected from file ***
*** loadspe. -> load specification of the semantics from file ***
*** listprg. -> display program ***
*** listspe. -> display specification ***
*** debugger. -> run debugger ***
*** save. -> save program to file ***
*** exit. -> leave program ***
*************************************************************************
>> loadprg.
Write the name of the program: 'evfibprg.pl'.
Program loaded.
>> loadspe.
Write the name of the program: 'evfibspe.pl'.
Specification loaded.
>> listprg.
**********************************************
*** DISPLAY PROGRAM. ***
**********************************************
fib(0) = s(0).
fib(s(0)) = s(0).
fib(s(s(_4566))) = sum(fib(s(_4566)),fib(_4566)).
sum(_4584,0) = _4584.
sum(_4598,s(_4596)) = s(sum(_4598,_4596)).
even(0) = true.
even(s(_4621)) = even(_4621).
**********************************************
**********************************************
>> listspe.
********************************************
*** DISPLAY SPECIFICATION. ***
********************************************
fib(0) = s(0).
fib(s(0)) = s(0).
fib(s(s(_5855))) = sum(fib(s(_5855)),fib(_5855)).
sum(_5873,0) = _5873.
sum(_5887,s(_5885)) = s(sum(_5887,_5885)).
even(0) = true.
even(s(s(_5910))) = even(_5910).
********************************************
********************************************
>> debugger.
************************************************
NARROWING STRATEGY OPTION
************************************************
1. Basic Narrowing.
2. Leftmost-Innermost Narrowing.
3. Leftmost-Outermost Narrowing.
4. Needed Narrowing.
Introduce the option: 2.
************************************************
*** OVER APPROXIMATION I+ ***
************************************************
fib(s(s(_12519))) = s(_12531).
fib(s(s(_12496))) = _12489.
even(s(s(_12467))) = _12482.
even(0) = true.
sum(_12436,s(_12424)) = s(_12434).
sum(_12412,0) = _12412.
fib(s(s(_12372))) = sum(_12384,_12385).
fib(s(0)) = s(0).
fib(0) = s(0).
even(_12315) = even(_12315).
true = true.
sum(_12288,_12289) = sum(_12288,_12289).
fib(_12273) = fib(_12273).
0 = 0.
s(_12247) = s(_12247).
************************************************
************************************************
The Over Approximation I(+) has been computed with 3 iterations.
Enter the number K of iterations for computing I(-) : 3.
************************************************
*** UNDER APPROXIMATION I- ***
************************************************
even(s(s(s(s(s(s(_58256))))))) = even(_58256).
even(s(s(s(s(0))))) = true.
sum(_58203,s(s(s(_58191)))) = s(s(s(sum(_58203,_58191)))).
sum(_58154,s(s(0))) = s(s(_58154)).
fib(s(s(s(s(_58102))))) = sum(sum(sum(fib(s(_58102)),fib(_58102)),fib(s(_58102))),fib(s(s(_58102)))).
fib(s(s(s(0)))) = sum(sum(s(0),fib(0)),fib(s(0))).
fib(s(s(0))) = sum(s(0),s(0)).
even(s(s(s(s(_57952))))) = even(_57952).
even(s(s(0))) = true.
sum(_57903,s(s(_57895))) = s(s(sum(_57903,_57895))).
sum(_57860,s(0)) = s(_57860).
fib(s(s(s(_57817)))) = sum(sum(fib(s(_57817)),fib(_57817)),fib(s(_57817))).
fib(s(s(0))) = sum(s(0),fib(0)).
even(s(s(_57732))) = even(_57732).
even(0) = true.
sum(_57687,s(_57683)) = s(sum(_57687,_57683)).
sum(_57650,0) = _57650.
fib(s(s(_57618))) = sum(fib(s(_57618)),fib(_57618)).
fib(s(0)) = s(0).
fib(0) = s(0).
even(_57539) = even(_57539).
true = true.
sum(_57512,_57513) = sum(_57512,_57513).
fib(_57497) = fib(_57497).
0 = 0.
s(_57471) = s(_57471).
************************************************
************************************************
************************************************
*** TR(I-) ***
************************************************
even(_81689) = even(_81689).
true = true.
sum(_81662,_81663) = sum(_81662,_81663).
fib(_81647) = fib(_81647).
0 = 0.
s(_81621) = s(_81621).
even(s(_81606)) = even(_81606).
even(s(s(s(_81581)))) = even(_81581).
even(s(s(s(s(s(_81548)))))) = even(_81548).
even(s(s(s(s(s(s(s(_81511)))))))) = even(_81511).
even(0) = true.
even(s(s(0))) = true.
even(s(s(s(s(0))))) = true.
even(s(s(s(s(s(s(0))))))) = true.
sum(_81383,s(_81379)) = s(sum(_81383,_81379)).
sum(_81346,s(s(_81340))) = s(s(sum(_81346,_81340))).
sum(_81303,s(s(s(_81293)))) = s(s(s(sum(_81303,_81293)))).
fib(s(s(0))) = s(sum(s(0),0)).
sum(_81214,s(s(s(s(_81200))))) = s(s(s(s(sum(_81214,_81200))))).
sum(_81159,0) = _81159.
sum(_81133,s(0)) = s(_81133).
sum(_81103,s(s(0))) = s(s(_81103)).
sum(_81069,s(s(s(0)))) = s(s(s(_81069))).
fib(s(s(_81025))) = sum(fib(s(_81025)),fib(_81025)).
fib(s(s(s(_80980)))) = sum(sum(fib(s(_80980)),fib(_80980)),fib(s(_80980))).
fib(s(s(s(s(_80906))))) = sum(sum(sum(fib(s(_80906)),fib(_80906)),fib(s(_80906))),fib(s(s(_80906)))).
fib(s(s(s(s(s(_80811)))))) = sum(sum(sum(sum(fib(s(_80811)),fib(_80811)),fib(s(_80811))),fib(s(s(_80811)))),fib(s(s(s(_80811))))).
fib(s(0)) = s(0).
fib(s(s(0))) = sum(s(0),fib(0)).
fib(s(s(s(0)))) = sum(sum(s(0),fib(0)),fib(s(0))).
fib(s(s(s(s(0))))) = sum(sum(sum(s(0),fib(0)),fib(s(0))),fib(s(s(0)))).
fib(0) = s(0).
fib(s(s(0))) = sum(s(0),s(0)).
fib(s(s(s(0)))) = sum(sum(s(0),s(0)),fib(s(0))).
************************************************
************************************************
************************************************
*** ERRORS ***
************************************************
Incorrect equation: even(s(_107434)) = even(_107434).
Incorrect rule: even(s(_107434)) = even(_107434).
CORRECTION OPTIONS
************************************************
1. Automatic correction.
2. Manual correction.
Enter option: 1.
************************************************
*** EXAMPLE GENERATION ***
************************************************
Enter a list of ground constructors
|: [0,s(0)].
************************************************
*** Positive Examples ***
************************************************
sum(s(0),s(s(s(s(0))))) = s(s(s(s(s(0))))).
sum(0,s(s(s(s(0))))) = s(s(s(s(0)))).
even(s(s(s(s(s(s(0))))))) = true.
sum(0,s(s(s(0)))) = s(s(s(0))).
sum(s(0),s(s(s(0)))) = s(s(s(s(0)))).
even(s(s(s(s(0))))) = true.
sum(s(0),s(s(0))) = s(s(s(0))).
sum(0,s(s(0))) = s(s(0)).
even(s(s(0))) = true.
sum(s(0),s(0)) = s(s(0)).
sum(0,s(0)) = s(0).
************************************************
************************************************
************************************************
*** Negative Examples ***
************************************************
even(s(0)) = true.
************************************************
************************************************
........
************************************************
*** Positive Examples covered by R ***
************************************************
sum(0,s(0)) = s(0).
sum(s(0),s(0)) = s(s(0)).
even(s(s(0))) = true.
sum(0,s(s(0))) = s(s(0)).
sum(s(0),s(s(0))) = s(s(s(0))).
even(s(s(s(s(0))))) = true.
sum(s(0),s(s(s(0)))) = s(s(s(s(0)))).
sum(0,s(s(s(0)))) = s(s(s(0))).
even(s(s(s(s(s(s(0))))))) = true.
sum(0,s(s(s(s(0))))) = s(s(s(s(0)))).
sum(s(0),s(s(s(s(0))))) = s(s(s(s(s(0))))).
************************************************
************************************************
The correction is
even(s(s(_163699))) = even(_163699).
fib(0) = s(0).
fib(s(0)) = s(0).
fib(s(s(_163654))) = sum(fib(s(_163654)),fib(_163654)).
sum(_163637,0) = _163637.
sum(_163621,s(_163619)) = s(sum(_163621,_163619)).
even(0) = true.