Localisation des erreurs par � slicing � dans les programmes logiques avec contraintes

Ulrich Neumerkel Technische Universität Wien

– techniques de slicing basées sur des transformations de programmes – fragments localisés doivent être changés

– facilite des lectures sélectives

– sans interaction d’usager

– explique les phénomènes suivants :

– échec inattendu (insuffisance)

– solution inattendue (incorrection)

– non terminaison

– monotonie indispensable (Prolog pure sans négation, CLP(FD) etc.)

Lectures des programmes

– lectures traditionnelles : déclaratives et opérationnelles

– lectures sélectives : raffiner par transformations généralisation : enlever des buts

père(Père) ← * masculin(Père), enfant de( E, Père).

spécialisation : ajouter des buts (spé. false/0 : tranche d’échec).

conjoint de(Époux, Épouse) ← false, époux épouse(Époux, Épouse).

conjoint de(Épouse, Époux) ←

époux épouse(Époux, Épouse).

+ facilitent les lectures des programmes plus volumineux + fidélité au code source, présentation simplifiée (rayer, cacher) + pas de nouveau formalisme comme les arbres de preuve, les traces + convient avec contraintes incomplètes

Localisation automatisée — explications

insuffisance (échec inattendu) : généralisation maximale qui échoue, explique inconsistance de données (data inconsistency) et erreurs de modélisation (modelling error)

incorrection (solution inattendue) : spécialisation maximale qui est vraie

(couramment avec false/0) non terminaison : spécialisation maximale qui ne se termine pas

Propriétés communes : + l’erreur dans le fragment implique l’erreur dans le programme original + changement du fragment obligatoire + aucune interaction avec l’usager (sauf continue) + donc pas d’erreurs introduites pendant le débogage ? notion slicing, ou plutôt program modification ?

Exemple : échec inattendu

← frère de(B, P). % insuffisance

frère de(F, P) ← dif(F,P), masculin(F), enfant de(F,V), masculin(V), enfant de(P,V), enfant de(F,M), enfant de(P,M), féminin(V). masculin(franz I). masculin(joseph II). masculin(leopold II).

féminin(maria theresia).

enfant de(joseph II, maria theresia). enfant de(joseph II, franz I). enfant de(leopold II, maria theresia). enfant de(leopold II, franz I).

1,

Exemple : échec inattendu de la généralisation maximale

← frère de(B, P). % insuffisance

frère de(F, P) ← * dif(F,P),

* masculin(F),

* enfant de(F,V), masculin(V),

* enfant de(P,V),

* enfant de(F,M),

* enfant de(P,M), féminin(V). masculin(franz I). masculin(joseph II). masculin(leopold II).

féminin(maria theresia).

enfant de(joseph II, maria theresia). enfant de(joseph II, franz I). enfant de(leopold II, maria theresia). enfant de(leopold II, franz I).

1, 2

Recherche des explications d’échec inattendu

– non-terminaison à cause des fragments généralisés → analyser la terminaison (cTI)

– complexité : sous-problème déjà NP-hard, pas d’approximation (Monotone Minimum Satisfying Assignment, Umans 1999) → chercher les minima locaux (un par un)

– � labeling � pour fragments généralisés souvent plus coûteux que l’original → adapter stratégie de � labeling �

Problème similaire : Explications dans PPC (Jussien)

– généralisation d’un système de contraintes

– beaucoup plus de contraintes que points de programme - plus coûteux

- explication lisible pour usager ?

– utilise une recherche entrelacée avec � labeling � Exemple : solution inattendue

↚ enfant de(K, E), enfant de(E, K). % incorrection

enfant de(joseph II, maria theresia). enfant de(joseph II, franz I). enfant de(leopold II, maria theresia). enfant de(marie antoinette, maria theresia). enfant de(maria theresia, marie antoinette). enfant de(leopold II, franz I).

1,

Exemple : solution inattendue de la spécialisation maximale

↚ enfant de(K, E), enfant de(E, K). % incorrection

enfant de(joseph II, maria theresia).← false. enfant de(joseph II, franz I).← false. enfant de(leopold II, maria theresia).← false. enfant de(marie antoinette, maria theresia). enfant de(maria theresia, marie antoinette). enfant de(leopold II, franz I).← false.

1, 2

Exemple : non terminaison

← ancêtre de(Anc, leopold I). % non terminaison enfant de(karl VI, leopold I). enfant de(maria theresia, karl VI). enfant de(joseph II, maria theresia). enfant de(leopold II, maria theresia). enfant de(leopold II, franz I). enfant de(marie antoinette, maria theresia). enfant de(franz I, leopold II).

ancêtre de(Anc,Desc) ←

enfant de(Desc,Anc). ancêtre de(Anc,Desc) ←

enfant de(Enf, Anc), ancêtre de(Enf, Desc).

1,

Exemple : non terminaison de la tranche d’échec minimale

← ancêtre de(Anc, leopold I)., false. % non terminaison

enfant de(karl VI, leopold I).← false.
enfant de(maria theresia, karl VI).← false.
enfant de(joseph II, maria theresia).← false.
enfant de(leopold II, maria theresia).← false.

enfant de(leopold II, franz I).

enfant de(marie antoinette, maria theresia).← false.

enfant de(franz I, leopold II).

ancêtre de(Anc,Desc) ←false,

enfant de(Desc,Anc). ancêtre de(Anc,Desc) ←

enfant de(Enf, Anc),

ancêtre de(Enf, Desc)., false.

1, 2.

← ancêtre de(Anc, leopold I). % non terminaison enfant de(karl VI, leopold I). enfant de(maria theresia, karl VI). enfant de(joseph II, maria theresia). enfant de(leopold II, maria theresia). enfant de(leopold II, franz I). enfant de(marie antoinette, maria theresia). enfant de(franz I, leopold II).

ancêtre de(Anc,Desc) ←

enfant de(Desc,Anc). ancêtre de(Anc,Desc) ←

ancêtre de(Enf, Desc), enfant de(Enf, Anc).

1,

← ancêtre de(Anc, leopold I)., false. % non terminaison

enfant de(karl VI, leopold I).← false.
enfant de(maria theresia, karl VI).← false.
enfant de(joseph II, maria theresia).← false.
enfant de(leopold II, maria theresia).← false.
enfant de(leopold II, franz I).← false.
enfant de(marie antoinette, maria theresia).← false.
enfant de(franz I, leopold II).← false.
ancêtre de(Anc,Desc) ← false,

enfant de(Desc,Anc). ancêtre de(Anc,Desc) ←

ancêtre de(Enf, Desc), false, enfant de(Enf, 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