BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Logical Testing: Hoare-style Specification Meets Executable Valida
 tion - Kathy Gray (University of Cambridge)
DTSTART:20081024T141500Z
DTEND:20081024T151500Z
UID:TALK14614@talks.cam.ac.uk
CONTACT:Boris Feigin
DESCRIPTION:Software is often tested with unit tests\, in which each proce
 dure is executed in isolation\, and its result compared with an expected v
 alue.  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 subs
 tantial programming effort to encode the postconditions\, with the post-co
 nditions themselves obscured by the test programming scaffolding. The corr
 espondence between Hoare logic and test specifications suggests directly u
 sing logical specifications for tests.  The resulting tests then serve the
  dual purpose of a formal specification for the procedure.\n\nWe show how 
 logical test specifications can be embedded within Java and how the result
 ing test specification language is compiled into Java\; this compilation a
 utomatically redirects mutations\, as in software transactional memory\, t
 o support imperative procedures. We also insert monitors into the tested p
 rogram for coverage analysis and error reporting.\n
LOCATION:GS15\, Computer Laboratory
END:VEVENT
END:VCALENDAR