Sciweavers

Share
JAR
2010

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

9 years 1 months ago
Proof-Guided Test Selection from First-Order Specifications with Equality
This paper deals with test case selection from axiomatic specifications whose axioms are quantifier-free first-order formulas with equality. We first 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 defined for algebraic specifications, to quantifier-free first-order specifications with equality. This method basically consists of a case analysis of the property under test (the test purpose) according to the specification axioms. It is based on a proof search for the different instances of the test purpose. Since the calculus is sound and complete, this allows us to provide a full 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 efficiently dealing with the equality pr...
Delphine Longuet, Marc Aiguier, Pascale Le Gall
Added 19 May 2011
Updated 19 May 2011
Type Journal
Year 2010
Where JAR
Authors Delphine Longuet, Marc Aiguier, Pascale Le Gall
Comments (0)
books