Logical Testing: Hoare-style Specification Meets Executable Validation

Add to your list(s) Download to your calendar using vCal

• Kathy Gray (University of Cambridge)
• Friday 24 October 2008, 15:15-16:15
• GS15, Computer Laboratory.

If you have a question about this talk, please contact Boris Feigin.

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.

This talk is part of the Computer Laboratory Programming Research Group Seminar series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Programming Research Group Seminar
• Department of Computer Science and Technology talks and seminars
• GS15, Computer Laboratory
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.