A New Procedure for Simultaneously Checking Completeness and Ground Confluence
Identifieur interne : 00AE41 ( Main/Merge ); précédent : 00AE40; suivant : 00AE42A New Procedure for Simultaneously Checking Completeness and Ground Confluence
Auteurs : Adel BouhoulaSource :
English descriptors
- KwdEn :
Abstract
Algebraic specifications provide a powerful method for the specification of abstract data types in programming languages and software systems. Completeness and ground confluence are fundamental notions for building algebraic specifications in a correct and modular way. Related works for checking ground confluence are based on the completion techniques or on the test that all critical pairs between axioms are valid w.r.t. a sufficient criterion for ground confluence. It is generally accepted that such techniques may be very inefficient even for very small specifications. Indeed, the completion procedure often diverges and there often exist many critical pairs of the axioms. In this paper, we present a new procedure for simultaneously checking completeness and ground confluence for specifications with free/non-free constructors and parameterized specifications. If the specification is not complete or not ground confluent, then our procedure will output the set of patterns on whose ground instances a function is not defined and it can easily identify the rules that break ground confluence. Our procedure is the first one which is complete and it always terminates under the assumption of an oracle for deciding (joinable-) inductive properties. In contrast to previous works, our method does not rely on completion techniques and does not require the computation of critical pairs of the axioms. The method has been implemented in the prover SPIKE. This system allowed us to prove the completeness and the ground confluence of many specifications in a completely automatic way where related techniques diverge or generate very complex proofs.
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: 002826
- to stream Crin, to step Curation: 002826
- to stream Crin, to step Checkpoint: 002035
Links to Exploration step
CRIN:bouhoula99eLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="157">A New Procedure for Simultaneously Checking Completeness and Ground Confluence</title></titleStmt><publicationStmt><idno type="RBID">CRIN:bouhoula99e</idno><date when="1999" year="1999">1999</date><idno type="wicri:Area/Crin/Corpus">002826</idno><idno type="wicri:Area/Crin/Curation">002826</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">002826</idno><idno type="wicri:Area/Crin/Checkpoint">002035</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">002035</idno><idno type="wicri:Area/Main/Merge">00AE41</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">A New Procedure for Simultaneously Checking Completeness and Ground Confluence</title><author><name sortKey="Bouhoula, Adel" sort="Bouhoula, Adel" uniqKey="Bouhoula A" first="Adel" last="Bouhoula">Adel Bouhoula</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>algebraic specifications</term><term>automata techniques</term><term>completeness</term><term>ground confluence</term><term>logic and formal verification</term><term>parameterization</term><term>rewriting systems</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="4863">Algebraic specifications provide a powerful method for the specification of abstract data types in programming languages and software systems. Completeness and ground confluence are fundamental notions for building algebraic specifications in a correct and modular way. Related works for checking ground confluence are based on the completion techniques or on the test that all critical pairs between axioms are valid w.r.t. a sufficient criterion for ground confluence. It is generally accepted that such techniques may be very inefficient even for very small specifications. Indeed, the completion procedure often diverges and there often exist many critical pairs of the axioms. In this paper, we present a new procedure for simultaneously checking completeness and ground confluence for specifications with free/non-free constructors and parameterized specifications. If the specification is not complete or not ground confluent, then our procedure will output the set of patterns on whose ground instances a function is not defined and it can easily identify the rules that break ground confluence. Our procedure is the first one which is complete and it always terminates under the assumption of an oracle for deciding (joinable-) inductive properties. In contrast to previous works, our method does not rely on completion techniques and does not require the computation of critical pairs of the axioms. The method has been implemented in the prover SPIKE. This system allowed us to prove the completeness and the ground confluence of many specifications in a completely automatic way where related techniques diverge or generate very complex proofs.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Merge
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00AE41 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 00AE41 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Merge
|type= RBID
|clé= CRIN:bouhoula99e
|texte= A New Procedure for Simultaneously Checking Completeness and Ground Confluence
}}
| This area was generated with Dilib version V0.6.33. |  |