(4040) Testing with T2 and Exploiting the Power of In-code Specifications

Technical long talk 50 min

Tuesday, 2008-06-24, 14:00 - 14:50, Arena 3

Wishnu Prasetya - Utrecht University (speaker)

Topics

• Testing tools

Download the presentation

Abstract

In-code specifications are specifications written directly in the
(Java) source code, and expressed in the same language as the source
code (thus in Java). In-code specifications are well known, in the form of  the 
"assert" statement, but its power is still mostly unexploited. This is 
really unfortunate, because in-code specifications really have a lot of benefit. 
To fully exploit them we need a more powerful tool than Java's own basic 
assertion checking mechanism. We recently released a tool, called T2, that gives 
this capability.

Though in-code specifications are not as abstract e.g. Z or JML, they are 
nevertheless declarative (e.g. they specify "what" a method should do, 
instead of "how"), and powerful.  E.g.  we can express class 
invariant, pre- and post-conditions, temporal properties, application models, 
etc. Examples can be found in T2Manual:

    http://www.cs.uu.nl/wiki/WP/T2Framework

Moreover programmers do not need to learn a new language. This is a huge 
advantage, since training programmers to learn a new language is expensive.
We also have no dependency on additional tools. E.g. despite its bright ideas, 
production use of JML is problematic, because until now no stable and up-to-date 
JML parser exists. In-code specifications are also very cheap to maintain. In 
constrast, specifications written in e.g. Z have to be continually kept 
consistent with your Java sources, but because Z and Java do not trivially match 
one-to-one, this likely leads to a maintenance nightmare.

T2 is a fully automatic unit testing tool. It relies on reflection to collect 
in-code specifications in a target class and uses them when needed as test 
oracles.

But T2 is actually a lot more than that. Whereas most other testing tools test 
each method in isolation, T2 is "sequence-based". It means that each 
test it generates is a sequence of calls (or field updates) to the methods of 
the target class. This has the effect that the methods are basically checking 
each other. Effectively, each test checks against the conjunction of all 
specifications of the methods in the sequence, plus Java's own built-in fault 
detection (e.g. division by 0), plus additional fault detection code that the 
programmer may build in each method in the sequence. This makes a pretty strong 
oracle! Note that even if each specification is individually weak, the 
conjunction of all of them is often much stronger.

Tools that test each method in isolation often need a quite complete 
specifications, in order to effectively generate meaningful tests, and to 
effectively detect faults. However this is not realistic: writing a complete 
specification of today's complex systems is almost impossible. In practice, 
perhaps only the most important methods of a class will be specified, and each 
individual specification may only expose just the most critical aspects of the 
corresponding method. In contrast, sequence based testing can remain to work 
even if the specifications we provide is very partial. This is very important, 
because developers can thus decide the level of details of their specifications, 
e.g. according to their budget constraint.

T2 is also very fast. Unlike most tools, it performs the testing on-the-fly 
(rather than by first generating Junit code). Doing so allows T2 to inject 
thousands of tests in less than a second. Testing with T2 feels thus almost 
interactive. Psychologically this is important. Programming is mostly a 
thinking-by-doing process. So, immediate feedback is important. If unit testing 
is as easy as asking the compiler to check syntax, programmers would be more 
compelled to write specifications. Perhaps simple ones first, but as their 
understanding of their own program increases, fast feedback would compel them to 
exploratively add details to their specifications. In effect this stimulates 
incremental development of specifications.

T2 can check for internal errors, run time exceptions, method specifications, 
class invariant, and even temporal properties. It comes with lots of options. 
The current release generates the tests mostly by randomization (e.g. when to 
choose which method to call next, or which integer to pass as a parameter). 
Still, experiments show that T2 can deliver 60 - 80% coverage, which is really 
not bad given that it costs almost no effort to use. 100% coverage is not 
possible; since the problem is in general undecidable. So the place of an 
automated testing tool is really not to replace hand crafted tests. Instead it 
should be used as a complement. T2 will make a strong complement.

Our techinique in T2 will also be presented in IEEE's International Conference 
on Software Testing, Verification and Validation (ICST) in Norway, April 2008.
However we hope to reach a wider public, in particular developers on the field, 
by submitting to a conference such as Jazoon.

The current release of T2 is freely available under a GPL licence.