October 27, 2009
Alan Mycroft
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.