Proof-Guided Test Selection from First-Order Specifications with Equality

Abstract : This paper deals with test case selection from axiomatic speci cations whose axioms are quanti er-free rst-order formulas with equality. We rst prove the existence of an ideal exhaustive test set to start the selection from. We then propose an extension of the test selection method called axiom unfolding, originally de ned for algebraic speci cations, to quanti er-free rst-order speci cations with equality. This method basically consists of a case analysis of the property under test (the test purpose) according to the speci cation axioms. It is based on a proof search for the di erent instances of the test purpose, thus allowing a sound and complete coverage of this property. The generalisation we propose allows to deal with any kind of predicate (not only equality) and with any form of axiom and test purpose (not only equations or Horn clauses). Moreover, it improves our previous works with e ciently dealing with the equality predicate, thanks to the paramodulation rule.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2010, 45 (4), pp.437-473
Liste complète des métadonnées

Littérature citée [30 références]  Voir  Masquer  Télécharger

https://hal-ecp.archives-ouvertes.fr/hal-00782871
Contributeur : Marc Aiguier <>
Soumis le : jeudi 11 avril 2013 - 16:36:02
Dernière modification le : vendredi 29 juin 2018 - 12:11:52
Document(s) archivé(s) le : vendredi 12 juillet 2013 - 02:55:08

Fichier

JAR.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00782871, version 1

Collections

Citation

Delphine Longuet, Marc Aiguier, Pascale Le Gall. Proof-Guided Test Selection from First-Order Specifications with Equality. Journal of Automated Reasoning, Springer Verlag, 2010, 45 (4), pp.437-473. 〈hal-00782871〉

Partager

Métriques

Consultations de la notice

224

Téléchargements de fichiers

107