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

Delphine Longuet (1) , Marc Aiguier (2) , Pascale Le Gall (2)

1 LSV - Laboratoire Spécification et Vérification [Cachan]
2 MAS - Mathématiques Appliquées aux Systèmes - EA 4037

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.

Domaines: Logique en informatique [cs.LO]

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