Skip to Main content Skip to Navigation
Journal articles

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.
Document type :
Journal articles
Complete list of metadata

Cited literature [30 references]  Display  Hide  Download
Contributor : Marc Aiguier Connect in order to contact the contributor
Submitted on : Thursday, April 11, 2013 - 4:36:02 PM
Last modification on : Monday, February 15, 2021 - 10:50:12 AM
Long-term archiving on: : Friday, July 12, 2013 - 2:55:08 AM


Files produced by the author(s)


  • HAL Id : hal-00782871, version 1


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⟩



Les métriques sont temporairement indisponibles