Abstract
Software is often tested with unit tests, in which each procedure is executed in isolation, and its result compared with an expected value. Individual tests correspond to Hoare triples used in program logics, with the pre-conditions encoded into the procedure initializations and the post-conditions encoded as assertions. Unit tests for procedures that modify structures in-place or that may terminate unexpectedly require substantial programming effort to encode the postconditions, with the post-conditions themselves obscured by the test programming scaffolding. The correspondence between Hoare logic and test specifications suggests directly using logical specifications for tests. The resulting tests then serve the dual purpose of a formal specification for the procedure.
We show how logical test specifications can be embedded within Java and how the resulting test specification language is compiled into Java; this compilation automatically redirects mutations, as in software transactional memory, to support imperative procedures. We also insert monitors into the tested program for coverage analysis and error reporting.
Chapter PDF
Similar content being viewed by others
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.
References
Allen, E., Chase, D., Hallett, J., Luchangco, V., Maessen, J.-W., Ryu, S., Steele Jr., G.L., Tobin-Hochstadt, S.: The Fortress language specification. Technical report, Sun (2007)
Bartezko, D., Fischer, C., Moller, M., Wehrheim, H.: Jass – Java with assertions. In: Workshop on Runtime Verification (2001)
Beck, K.: Simple smalltalk testing with patterns. The Smalltalk Report (1994)
Beck, K., Gamma, E.: Test-infected: programmers love writing tests. Java Report (1998)
Beust, C., Suleiman, H.: Next Generation Java Testing: TestNG and Advanced Concepts. Addison-Wesley, Reading (2007)
Cheon, Y., Leavens, G.T.: A simple and practical approach to unit testing: The JML and JUnit way. In: Magnusson, B. (ed.) ECOOP 2002. LNCS, vol. 2374, p. 231. Springer, Heidelberg (2002)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proc. PLDI (2002)
Freeman, S., Pryce, N.: Evolving an embedded domain-specific language in Java. In: Proc. OOPSLA (2006)
Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 3rd edn. Addison-Wesley, Reading (2005)
King, G.: LIFT — the lisp framework for testing. Technical Report 01-25, U. Mass. CS (2001)
Leavens, G.T., Baker, A.L., Ruby, C.: JML: A Notation for Detailed Design, ch. 12. Kluwer, Dordrecht (1999)
Shavit, N., Touitou, D.: Software transactional memory. In: Principles of Distributed Computing (1995)
Welsh, N., Solsona, F., Glover, I.: SchemeUnit and SchemeQL: Two little languages. In: Proc. Scheme Workshop (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gray, K.E., Mycroft, A. (2009). Logical Testing. In: Chechik, M., Wirsing, M. (eds) Fundamental Approaches to Software Engineering. FASE 2009. Lecture Notes in Computer Science, vol 5503. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00593-0_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-00593-0_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00592-3
Online ISBN: 978-3-642-00593-0
eBook Packages: Computer ScienceComputer Science (R0)