Slicing zur Fehlersuche in (Constraint-) Logikprogrammen

Stefan Kral, Fred Mesnard, Ulrich Neumerkel Technische Universität Wien, Université de la Réunion

• transformationsbasierte Slicing-Techniken

• lokalisieren Programmteile, die geändert werden müssen

• unterstützen Lesarten

• keine Benutzerinteraktion

• alle üblichen Fehlerarten – fehlende Lösungen (insufficiency)

– unerwartete Lösung (incorrectness)

– Nichttermination

• Monotonie erforderlich (pures Prolog ohne Negation, CLP(FD) etc.)

Lesarten

• Traditionell: deklarativ und prozedural

• Verfeinerung der Lesarten durch Transformationen:

Verallgemeinerung: Löschen von Zielen.

vater(Vater) ← * männlich(Vater), kind von( Kind, Vater).

Spezialisierung: Hinzufügen von Zielen (v.a. false/0).

verheiratet mit(Gatte, Gattin) ← false,

gatte gattin(Gatte, Gattin). verheiratet mit(Gattin, Gatte) ← gatte gattin(Gatte, Gattin).

+ ermöglicht informelles Lesen größerer Programme + Quelltexttreue, einfache Veranschaulichung (Durchstreichen, Zudecken) + für (unvollständige) Constraints geeignet, kein neuer Formalismus wie

Beweisbaum, Trace etc.

Slicing zur Fehlersuche

fehlende Lösung: maximale Verallgemeinerung, die scheitert

erklärt data inconsistency und modelling error unerwartete Lösung: maximale Spezialisierung, die erfüllt ist (momentan

nur mit false/0) Nichttermination: maximale Spezialisierung, die nicht terminiert. Gemeinsame Eigenschaften: + Fehler in Fragment bedingt Fehler im ursprünglichen Programm + Fragment muß verändert werden + keine Benutzerinteraktion (daher keine Bedienungsfehler) ? noch slicing, oder schon program modification?

Beispiel: Fehlende Lösung

← bruder von(B, P). % Fehler

bruder von(B, P) ← dif(B,P), männlich(B), kind von(B,V), männlich(V), kind von(P,V), kind von(B,M), kind von(P,M), weiblich(V). männlich(franz I). männlich(joseph II). männlich(leopold II).

weiblich(maria theresia).

kind von(joseph II, maria theresia). kind von(joseph II, franz I). kind von(leopold II, maria theresia). kind von(leopold II, franz I).

1,

Beispiel: Fehlende Lösung in maximaler Verallgemeinerung

← bruder von(B, P). % Fehler

bruder von(B, P) ← * dif(B,P),

* männlich(B),

* kind von(B,V), männlich(V),

* kind von(P,V),

* kind von(B,M),

* kind von(P,M), weiblich(V). männlich(franz I). männlich(joseph II). männlich(leopold II).

weiblich(maria theresia).

kind von(joseph II, maria theresia). kind von(joseph II, franz I). kind von(leopold II, maria theresia). kind von(leopold II, franz I).

1, 2

Beispiel: Unerwartete Lösung

↚ kind von(K, E), kind von(E, K). % Fehler

kind von(joseph II, maria theresia). kind von(joseph II, franz I). kind von(leopold II, maria theresia). kind von(marie antoinette, maria theresia). kind von(maria theresia, marie antoinette). kind von(leopold II, franz I).

1,

Beispiel: Unerwartete Lösung in maximaler Spezialisierung

↚ kind von(K, E), kind von(E, K). % Fehler

kind von(joseph II, maria theresia).← false. kind von(joseph II, franz I).← false. kind von(leopold II, maria theresia).← false. kind von(marie antoinette, maria theresia). kind von(maria theresia, marie antoinette). kind von(leopold II, franz I).← false.

1, 2

Example: Nonterminating program

← ancestor of(Anc, leopold I). % Does not terminate child of(karl VI, leopold I). child of(maria theresia, karl VI). child of(joseph II, maria theresia). child of(leopold II, maria theresia). child of(leopold II, franz I). child of(marie antoinette, maria theresia). child of(franz I, leopold II).

ancestor of(Anc,Desc) ←

child of(Desc,Anc). ancestor of(Anc,Desc) ←

child of(Child, Anc),

ancestor of(Child, Desc).

1,

Example: Nonterminating program and minimal failure slice

← ancestor of(Anc, leopold I)., false. % Does not terminate

child of(karl VI, leopold I).← false.
child of(maria theresia, karl VI).← false.
child of(joseph II, maria theresia).← false.
child of(leopold II, maria theresia).← false.

child of(leopold II, franz I).

child of(marie antoinette, maria theresia).← false.

child of(franz I, leopold II).

ancestor of(Anc,Desc) ←false,

child of(Desc,Anc). ancestor of(Anc,Desc) ←

child of(Child, Anc),

ancestor of(Child, Desc)., false.

1, 2.

Example: Nonterminating program

← ancestor of(Anc, leopold I). % Does not terminate child of(karl VI, leopold I). child of(maria theresia, karl VI). child of(joseph II, maria theresia). child of(leopold II, maria theresia). child of(leopold II, franz I). child of(marie antoinette, maria theresia). child of(franz I, leopold II).

ancestor of(Anc,Desc) ←

child of(Desc,Anc). ancestor of(Anc,Desc) ←

ancestor of(Child, Desc), child of(Child, Anc).

1,

Example: Nonterminating program and minimal failure slice

← ancestor of(Anc, leopold I)., false. % Does not terminate

child of(karl VI, leopold I).← false.
child of(maria theresia, karl VI).← false.
child of(joseph II, maria theresia).← false.
child of(leopold II, maria theresia).← false.
child of(leopold II, franz I).← false.
child of(marie antoinette, maria theresia).← false.
child of(franz I, leopold II).← false.
ancestor of(Anc,Desc) ← false,

child of(Desc,Anc). ancestor of(Anc,Desc) ←

ancestor of(Child, Desc), false, child of(Child, Anc).

1, 2.

missing termination proof

← phrase(regexp(Expr), Xs0,Xs) terminates if

finiteground(Expr), boundlist(Xs0). regexp([]) ⟶

[]. regexp([E]) ⟶

[E]. regexp({ Expr}) ⟶

[]. regexp({Expr}) ⟶

regexp(Expr), regexp({Expr}).

regexp(A*B) ⟶ regexp(A), regexp(B).

1,

Min.f-slice explains missing termination proof

← phrase(regexp(Expr), Xs0,Xs) terminates if

finiteground(Expr), boundlist(Xs0). regexp([]) ⟶

[].

regexp([E]) ⟶ {false},

[E].

regexp({ Expr}) ⟶ {false},

[]. regexp({Expr}) ⟶

regexp(Expr), regexp({Expr})., {false}.

regexp(A*B) ⟶ {false},

regexp(A), regexp(B).

1, 2,

?: Min.f-slice explains with subst’s missing termination proof

← Expr = {[]}, phrase(regexp(Expr), Xs0,Xs) terminates if

finiteground(Expr), boundlist(Xs0). regexp([]) ⟶

[].

regexp([E]) ⟶ {false},

[E].

regexp({ Expr}) ⟶ {false},

[]. regexp({Expr}) ⟶ {Expr = []}, % ... not yet implemented ...

regexp(Expr), regexp({Expr})., {false}.

regexp(A*B) ⟶ {false},

regexp(A), regexp(B).

1, 2, 3.

URLs

http://www.univ-reunion.fr/~gcc
http://www.complang.tuwien.ac.at/ulrich