Quick Checking Your Java Classes With T2

Stc
Date: 2007-11-01

Time: 11:45

Room: BBL room 471

Speaker: Wishnu Prasetya

Title: QuickChecking your Java Classes with T2

Abstract

T2 is our recently home brewed automated testing tool for Java. It was inspired by the success of QuickCheck. However, objects are quite different from functions; so quite early in its design T2 had to take a very different random testing strategy.

Most automated testing tools for Java would test a class C by testing each of its methods in isolation. Such an approach works poorly if specifications are only partial, which is usually the case in practice. Unlike QuickCheck they also first generate Junit scripts, which have to be executed first to actually do the testing. In contrast, T2 generates sequences of calls to the methods of C that are checked on-the-fly. This is more interactive, and has the side effect that methods are checking each other. Although simple, it seems to work quite well, even when specifications are only partially provided. T2 can check internal errors, Hoare triple specifications, class invariant, and even temporal properties.

In this 45 minutes presentation I'll show you how it works. I will also show you another nice feature of T2. It doesn't require you to write specifications in e.g. JML or Z. You write specifications directly in Java. This is called ’in-code’ specifications. It is actually quite powerful; I will show you.

  • Tool site and download: here.