Programs, Properties, and Data: Exploring the Software Development Trilogy

Abstract : Software development usually involves a collection of properties, programs and data as input or output documents. Putting these three kinds of documents at the vertices of a triangle, one sees that all three sides of the triangle have been exploited in formal methods, and that they have often been used in both directions. However, richer combinations have seldom been envisaged, and formal methods often amount to a strict orientation of the figure by imposing functional dependencies (e.g., infering test cases from specifications). Moreover, undecidability problems arise when properties are expressed in full predicate logic (or similar formalisms) or programs are written in Turing-equivalent programming languages. We advocate that (1) formal methods should provide more flexible ways to exploit the developer's knowledge and offer a variety of possibilities to construct programs, properties and test data and (2) it is worth restricting the power of logic formalisms and programming languages for the benefit of mechanization. We go one step in this direction, and present a formal method for generating test cases that combines techniques from abstract interpretation (program->property) and testing (program+property->test data), and takes inspiration from automated learning (test generation via a testing bias). The crucial property of the test suites generated this way is that they are robust with respect to a test objective formalized as a property. In other words, if a program passes the test suite, then it is guaranteed to satisfy the property. As this process leads to decision problems in very restricted formalisms, it can be fully mechanized.
Type de document :
Article dans une revue
IEEE Software, Institute of Electrical and Electronics Engineers, 1998, 15 (6), pp.75-81. 〈10.1109/52.730849〉
Liste complète des métadonnées

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

http://hal.univ-brest.fr/hal-00783203
Contributeur : Valérie-Anne Nicolas <>
Soumis le : vendredi 1 février 2013 - 11:09:42
Dernière modification le : mercredi 16 mai 2018 - 11:23:14
Document(s) archivé(s) le : jeudi 2 mai 2013 - 04:01:10

Fichier

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

Identifiants

Citation

Daniel Le Métayer, Valérie-Anne Nicolas, Olivier Ridoux. Programs, Properties, and Data: Exploring the Software Development Trilogy. IEEE Software, Institute of Electrical and Electronics Engineers, 1998, 15 (6), pp.75-81. 〈10.1109/52.730849〉. 〈hal-00783203〉

Partager

Métriques

Consultations de la notice

552

Téléchargements de fichiers

132