Programs, Properties, and Data: Exploring the Software Development Trilogy - Université de Bretagne Occidentale Accéder directement au contenu
Article Dans Une Revue IEEE Software Année : 1998

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

Résumé

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.
Fichier principal
Vignette du fichier
LMNR98.pdf (126.85 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00783203 , version 1 (01-02-2013)

Identifiants

Citer

Daniel Le Métayer, Valérie-Anne Nicolas, Olivier Ridoux. Programs, Properties, and Data: Exploring the Software Development Trilogy. IEEE Software, 1998, 15 (6), pp.75-81. ⟨10.1109/52.730849⟩. ⟨hal-00783203⟩
391 Consultations
231 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More