BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Computer Laboratory Programming Research Group Sem
 inar
SUMMARY:Logical Testing: Hoare-style Specification Meets E
 xecutable Validation - Kathy Gray (University of C
 ambridge)
DTSTART;TZID=Europe/London:20081024T151500
DTEND;TZID=Europe/London:20081024T161500
UID:TALK14614AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/14614
DESCRIPTION:Software is often tested with unit tests\, in whic
 h each procedure is executed in isolation\, and it
 s result compared with an expected value.  Individ
 ual tests correspond to Hoare triples used in prog
 ram logics\, with the pre-conditions encoded into 
 the procedure initializations and the post-conditi
 ons encoded as assertions. Unit tests for procedur
 es that modify structures in-place or that may ter
 minate unexpectedly require substantial programmin
 g effort to encode the postconditions\, with the p
 ost-conditions themselves obscured by the test pro
 gramming scaffolding. The correspondence between H
 oare logic and test specifications suggests direct
 ly using logical specifications for tests.  The re
 sulting tests then serve the dual purpose of a for
 mal specification for the procedure.\n\nWe show ho
 w logical test specifications can be embedded with
 in Java and how the resulting test specification l
 anguage is compiled into Java\; this compilation a
 utomatically redirects mutations\, as in software 
 transactional memory\, to support imperative proce
 dures. We also insert monitors into the tested pro
 gram for coverage analysis and error reporting.\n
LOCATION:GS15\, Computer Laboratory
CONTACT:Boris Feigin
END:VEVENT
END:VCALENDAR