IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Software Seminar Series > 2009 > Program Testing via Hoare-style Specifications
Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

Alan Mycroft

martes 27 de octubre de 2009

11:00am Meeting room 302 (Mountain View), level 3

Alan Mycroft, Invited researcher, IMDEA Software Institute

Program Testing via Hoare-style Specifications

Abstract:

Program Validation (testing) and Verification (formal proof) are too often seen as disjoint subject areas. We observe that a typical “unit test” (e.g. in JUnit) first creates some data structure, then invokes the procedure under test, then checks an assertion –in essence a Hoare Triple {P}C{Q} but opaquely coded. The Hoare-triple view of tests greatly simplifies the coding of tests, expecially for procedures which mutate data structures or raise exceptions. Such tests can be implemented using transactional memory to provide access to both x and old(x), and for more high-level constructs such as modifiesonly(x.f,y.g). We show how such tests may be compiled into standard Java. Moreover, this view encourages generalised tests in which preconditions can use logical forms such as “forall” and implication. Transactional techniques allow such generalised tests to be used during execution on real data as a form of a test mode. This is joint work with Kathryn Gray, extending FASE'2009 work.