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.

This talk shows how logical test specifications can be embedded within Java and how these specifications may be compiled into Java. We show how, during compilation, we can redirect mutations during tests to assess modifications made by imperative methods, using software transactional memory. We also show how embedding test specifications within the language simplifies integration with a test engine while providing detailed reports and test-specific coverage analysis.