Skip to Main content Skip to Navigation
Journal articles

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.
Document type :
Journal articles
Complete list of metadatas

Cited literature [16 references]  Display  Hide  Download

https://hal.univ-brest.fr/hal-00783203
Contributor : Valérie-Anne Nicolas <>
Submitted on : Friday, February 1, 2013 - 11:09:42 AM
Last modification on : Wednesday, August 5, 2020 - 3:45:14 AM
Long-term archiving on: : Thursday, May 2, 2013 - 4:01:10 AM

File

LMNR98.pdf
Files produced by the author(s)

Identifiers

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⟩

Share

Metrics

Record views

899

Files downloads

254