Abstract
In this paper, we explore the testing-verification relationship with the objective of mechanizing the generation of test data. We consider program classes defined as recursive program schemes and we show that complete and finite test data sets can be associated with such classes, that is to say that these test data sets allow us to distinguish every two different functions in these schemes. This technique is applied to the verification of simple properties of programs.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)
Budd, T.A., Angluin, D.: Two Notions of Correctness and Their Relation to Testing. Acta Informatica 18 (1982)
Beizer, B.: Software Testing Techniques, 2nd Edition. Van Nostrand Reinhold (1990)
Bergadano, F., Gunetti, D.: Testing by means of inductive program learning. ACM transactions on Software Engineering and Methodo- logy 5(2) (1996)
Biermann, A.: The inference of regular LISP programs from examples. IEEE transactions on Systems, Man, and Cybernetics 8(8) (1978)
Bochmann, G.V., Petrenko, A.: Protocol Testing: Review of Me- thods and Relevance for Software Testing. In: Proceedings of ISSTA (August 1994)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th POPL (1977)
Demillo, R.A., Offutt, A.J.: Constraint-Based Automatic Test Data Generation. IEEE Transactions on Software Engineering 17(9) (September 1991)
Fernandez, J.-C., Jard, C., Jéron, T., Viho, C.G.: Using on- the-fly verification techniques for the generation of test suites. In: Proceedings of the Conference on Computer-Aided Verification (July 1996)
Freedman, R.S.: Testability of Software Components. IEEE Transactions on Software Engineering 17(6) (June 1991)
Gaudel, M.-C.: Testing can be formal, too. In: Proceedings of TAPSOFT (1995)
Goodenough, J.B., Gerhart, S.L.: Toward a Theory of Test Data Selection. IEEE Transactions on Software Engineering 1(2) (June 1975)
Guttag, J.V., Horning, J.J.: Larch: languages and tools for formal specification. Texts and Monographs in Computer Science (1993)
Jones, C.B.: Systematic software development using VDM, 2nd edn. Prentice Hall International, Englewood Cliffs (1990)
Le MéTayer, D.: Program analysis for software engineering: new appli- cations, new requirements, new tools. ACM Sigplan Notices (1) (Janvier 1997)
Le MéTayer, D., Nicolas, V.-A., Ridoux, O.: Exploring the Software Development Trilogy. IEEE Software (November 1998)
Nicolas, V.-A.: Preuves de Propriétés de Classes de Programmes par Dérivation Systématique de Jeux de Test. PhD thesis, Université de Ren- nes 1 (December 1998)
Ntafos, S.C.: A Comparison of Some Structural Testing Strategies. IEEE Transactions on Software Engineering 14(6) (June 1988)
Ostrand, T.J., Weyuker, E.J.: Data Flow-Based Test Adequacy Analysis for Languages with Pointers. In: Proceedings of POPL (January 1991)
Pierce, B., Dietzen, S., Michaylov, S.: Programming in Higher- Order Typed Lambda-Calculi. Research report CMU-CS-89-111 (March 1989)
Richardson, D.J., Clarke, L.A.: Partition Analysis: A Method Combining Testing and Verification. IEEE Transactions on Software Engineering 11(12) (December 1985)
Rapps, S., Weyuker, E.J.: Selecting Software Test Data Using Dataflow Information. IEEE Transactions on Software Engineering 11(4) (April 1985)
Spivey, M.: The Z notation - A reference manual, 2nd edn. International Series in Computer Science. Prentice Hall International, Englewood Cliffs (1992)
Weyuker, E.J.: Assessing test data adequacy through program inference. ACM Transactions on Programming Languages and Systems 5(4) (October 1983)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Le Métayer, D., Nicolas, VA., Ridoux, O. (2000). Verification by Testing for Recursive Program Schemes. In: Bossi, A. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 1999. Lecture Notes in Computer Science, vol 1817. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10720327_15
Download citation
DOI: https://doi.org/10.1007/10720327_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67628-7
Online ISBN: 978-3-540-45148-8
eBook Packages: Springer Book Archive
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.