Correction de conjectures fausses par synthèse de programmes

Autor: Demba, Moussa, Alexandre, Francis, Bsaïes, Khaled
Přispěvatelé: Development of specifications (DEDALE), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP)-Institut National de Recherche en Informatique et en Automatique (Inria), Ducassé, Mireille, Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), Loria, Publications
Jazyk: francouzština
Rok vydání: 2003
Předmět:
Zdroj: Douzièmes Journées Francophones de Programmation Logique et Programmation par Contraintes 2003-JFPLC'2003
Douzièmes Journées Francophones de Programmation Logique et Programmation par Contraintes 2003-JFPLC'2003, 2003, Amiens, France, 4 p
Popis: Colloque avec actes et comité de lecture. internationale.; International audience; Dans le domaine de la vérification, les preuves ne terminent pas toujours avec succès, à cause des formules non prouvables. Parfois, le prouveur signale simplement l'échec. Cependant, dans certains cas il est intéressant de connaître la cause de cet échec et de la corriger. Les méthodes classiques sont insuffisantes pour qu'un prouveur détecte et corrige automatiquement les incohérences dans les programmes ou les formules logiques. Dans cet article, nous proposons une méthode permettant de corriger de formules fausses. Soit $ \Phi(x)$ une formule fausse, la méthode présentée consiste à construire un prédicat de correction $P$ tel que $\forall x~(\Phi(x)\Leftarrow P(x))$ soit valide.
Databáze: OpenAIRE
Externí odkaz: