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 metadatas

Cited literature [30 references]  Display  Hide  Download

https://hal-ecp.archives-ouvertes.fr/hal-00782871
Contributor : Marc Aiguier <>
Submitted on : Thursday, April 11, 2013 - 4:36:02 PM
Last modification on : Tuesday, December 18, 2018 - 3:32:10 PM
Long-term archiving on : Friday, July 12, 2013 - 2:55:08 AM

File

JAR.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

270

Files downloads

140