A New Technique for Verifying and Correcting Logic Programs
Identifieur interne : 00BC89 ( Main/Exploration ); précédent : 00BC88; suivant : 00BC90A New Technique for Verifying and Correcting Logic Programs
Auteurs : Ricardo Caferra [France] ; Nicolas Peltier [France]Source :
- Journal of Automated Reasoning [ 0168-7433 ] ; 1997-12-01.
English descriptors
Abstract
Abstract: A significant extension to a model-building method that we have beendeveloping for several years is presented. A quite complete, albeitreasonably short, description of the previous method is given in order tomake this article self-contained. The extension enables the handling ofPresburger arithmetic and the deducing of inductive consequences from setsof Horn clauses. For a large class of logic programs the extension alsopermits the deduction of negative facts and the detection of nontermination.It is shown how the extended method can be used in verifying and correctingprograms. The proposed method verifies programs w.r.t. formalspecifications, but its fundamentals (i.e., model building) make it usefulfor pointing out errors and for suggesting a way of correcting wrongprograms also w.r.t. informal specifications, such as specifications byexamples or specifications using implicit knowledge (the latter features areespecially useful when dealing with beginners’ programs). Theoreticalproperties of the extended method (e.g., soundness and refutationalcompleteness) are proven. The greater power of the extensions to logicprogramming enabled by our method relative to existing methods and withrespect to other standard features (like negation as failure) is alsoproven. Several nontrivial examples illustrate error detection andcorrection as well as the broadening of inference capabilities that can beobtained in logic programming by using the rules of this method. Thesedetailed examples show evidence of the interest of our approach. Maindirections for future research are given.
Url:
DOI: 10.1023/A:1005878609884
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 002D75
- to stream Istex, to step Curation: 002D38
- to stream Istex, to step Checkpoint: 002822
- to stream Main, to step Merge: 00C467
- to stream Main, to step Curation: 00BC89
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">A New Technique for Verifying and Correcting Logic Programs</title><author><name sortKey="Caferra, Ricardo" sort="Caferra, Ricardo" uniqKey="Caferra R" first="Ricardo" last="Caferra">Ricardo Caferra</name></author><author><name sortKey="Peltier, Nicolas" sort="Peltier, Nicolas" uniqKey="Peltier N" first="Nicolas" last="Peltier">Nicolas Peltier</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:C0CC2EE5B2D1C11732C320E9A57E10FDE184CE3B</idno><date when="1997" year="1997">1997</date><idno type="doi">10.1023/A:1005878609884</idno><idno type="url">https://api.istex.fr/ark:/67375/VQC-2JNSLS38-M/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002D75</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002D75</idno><idno type="wicri:Area/Istex/Curation">002D38</idno><idno type="wicri:Area/Istex/Checkpoint">002822</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">002822</idno><idno type="wicri:doubleKey">0168-7433:1997:Caferra R:a:new:technique</idno><idno type="wicri:Area/Main/Merge">00C467</idno><idno type="wicri:Area/Main/Curation">00BC89</idno><idno type="wicri:Area/Main/Exploration">00BC89</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">A New Technique for Verifying and Correcting Logic Programs</title><author><name sortKey="Caferra, Ricardo" sort="Caferra, Ricardo" uniqKey="Caferra R" first="Ricardo" last="Caferra">Ricardo Caferra</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>Leibniz Laboratory, Imag, 46, Avenue Félix Viallet, 38031, Grenoble Cedex</wicri:regionArea><placeName><region type="region" nuts="2">Auvergne-Rhône-Alpes</region><region type="old region" nuts="2">Rhône-Alpes</region><settlement type="city">Grenoble</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author><author><name sortKey="Peltier, Nicolas" sort="Peltier, Nicolas" uniqKey="Peltier N" first="Nicolas" last="Peltier">Nicolas Peltier</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>Leibniz Laboratory, Imag, 46, Avenue Félix Viallet, 38031, Grenoble Cedex</wicri:regionArea><placeName><region type="region" nuts="2">Auvergne-Rhône-Alpes</region><region type="old region" nuts="2">Rhône-Alpes</region><settlement type="city">Grenoble</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author></analytic><monogr></monogr><series><title level="j">Journal of Automated Reasoning</title><title level="j" type="abbrev">Journal of Automated Reasoning</title><idno type="ISSN">0168-7433</idno><idno type="eISSN">1573-0670</idno><imprint><publisher>Kluwer Academic Publishers</publisher><pubPlace>Dordrecht</pubPlace><date type="published" when="1997-12-01">1997-12-01</date><biblScope unit="volume">19</biblScope><biblScope unit="issue">3</biblScope><biblScope unit="page" from="277">277</biblScope><biblScope unit="page" to="318">318</biblScope></imprint><idno type="ISSN">0168-7433</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0168-7433</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>logic programming</term><term>model building</term><term>program verification</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: A significant extension to a model-building method that we have beendeveloping for several years is presented. A quite complete, albeitreasonably short, description of the previous method is given in order tomake this article self-contained. The extension enables the handling ofPresburger arithmetic and the deducing of inductive consequences from setsof Horn clauses. For a large class of logic programs the extension alsopermits the deduction of negative facts and the detection of nontermination.It is shown how the extended method can be used in verifying and correctingprograms. The proposed method verifies programs w.r.t. formalspecifications, but its fundamentals (i.e., model building) make it usefulfor pointing out errors and for suggesting a way of correcting wrongprograms also w.r.t. informal specifications, such as specifications byexamples or specifications using implicit knowledge (the latter features areespecially useful when dealing with beginners’ programs). Theoreticalproperties of the extended method (e.g., soundness and refutationalcompleteness) are proven. The greater power of the extensions to logicprogramming enabled by our method relative to existing methods and withrespect to other standard features (like negation as failure) is alsoproven. Several nontrivial examples illustrate error detection andcorrection as well as the broadening of inference capabilities that can beobtained in logic programming by using the rules of this method. Thesedetailed examples show evidence of the interest of our approach. Maindirections for future research are given.</div></front></TEI><affiliations><list><country><li>France</li></country><region><li>Auvergne-Rhône-Alpes</li><li>Rhône-Alpes</li></region><settlement><li>Grenoble</li></settlement></list><tree><country name="France"><region name="Auvergne-Rhône-Alpes"><name sortKey="Caferra, Ricardo" sort="Caferra, Ricardo" uniqKey="Caferra R" first="Ricardo" last="Caferra">Ricardo Caferra</name></region><name sortKey="Caferra, Ricardo" sort="Caferra, Ricardo" uniqKey="Caferra R" first="Ricardo" last="Caferra">Ricardo Caferra</name><name sortKey="Peltier, Nicolas" sort="Peltier, Nicolas" uniqKey="Peltier N" first="Nicolas" last="Peltier">Nicolas Peltier</name><name sortKey="Peltier, Nicolas" sort="Peltier, Nicolas" uniqKey="Peltier N" first="Nicolas" last="Peltier">Nicolas Peltier</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00BC89 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00BC89 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:C0CC2EE5B2D1C11732C320E9A57E10FDE184CE3B
|texte= A New Technique for Verifying and Correcting Logic Programs
}}
| This area was generated with Dilib version V0.6.33. |  |