Transcript powerpoint

Quick Checking Your Java Classes
With T2
Wishnu Prasetya
Dept. of Information & Computing Sciences
Utrecht University
www.cs.uu.nl/~wishnu
Overview






What is T2, and its key ideas
Implementation
Programming Specifications
Related Work
Result & Research Status
Conclusion
2
T2 = Testing Tool 

A tool to automatically test a Java class
with some interesting features ...

Unit testing.

Inspired by QuickCheck
3
QuickCheck and T2

Both generates tests randomly

Not pure random, but with some direction


passive direction from specs.
One is for functional, the other for OO
4
Example : my own sorted list
public class SortedList {
private LinkedList<Comparable> s
private Comparable max
public SortedList()
// initialize s to empty
public void insert(Comparable x)
public Comparable get()
}
5
In-code Specification
public boolean classinv() {
return
s.isEmpty()  s.contains(max)
public Comparable get_spec() {
public class SortedList {
}
assert s.isEmpty() : "PRE"
private LinkedList<Comparable> s
Comparable ret = get()
private Comparable max
assert …  ret.compareTo(s.getLast())  0 : "POST"
public SortedList()
return ret
Less abstract
} public void insert(Comparable x)
Cannot guarantee non-interference
Declarative
public Comparable get() // return and remove max
Powerful
Minimum maintenance
}
6
What if my specification is partial ?
private s
private max
No pre/post-conditions
Class inv. Is partial
// classinv : s.isEmpty()  s.contains(max)
public void insert(Comparable x) {
int i = 0
for (Comparable y : s) {
if (y.compareTo(x) > 0) break
i++ }
s.add(i,x)
if (max==null || x.compareTo(max) < 0) max = x
}
Most tools do isolated testing; it will
Leak faults
produce losts of false positives
7
Sequences as Tests

Simplification


We only have private and public members
Updating a field F is represented by a call to setF

We’ll talk about a class C

A test on C is: a (finite) sequence of calls to
pubmeth(C)
8
Back to example
private s
private max
Hey, with sequence I can catch the fault, despite
my partial spec!
It also autogenerates ‘interesting’ target objects.
// classinv : s.isEmpty()  s.contains(max)
public void insert(Comparable x) // faulty
public Comparable get() // return and remove max
public Comparable get_spec() {
u = new SortedList<Integer>
assert !s.isEmpty() : "PRE"
u.insert(1) ; u.insert(10)
Comparable ret = get()
u.get()
assert …  ret.compareTo(s.getLast())  0 : "POST"
return ret
}
9
Functions vs Objects

f :: A  B



Its behavior is fully determined by the relation between
its parameter and result.
Deterministic.
An object u:C



Its behavior (transition from state to state) is
determined by all C’s methods.
Non-deterministic.
From this persperctive it is natural to use sequence.
10
Implementation
1.
2.
Representation of tests
T2 algorithm
Representing a test
void test1 () {

As a Java (Jtest) code
Most testing tools do this...

try { u = new SortedList<Integer>
u.insert(1) ; u.insert(10)
u.get_spec() }
catch (AssertError e) …
Alternatively, represent a test as ordinary data


In Haskell you can exploit higher order functions
In Java  object. Possible via “meta” objects from
Reflection library.
12
Meta representation of a test
This is just a list of objects; you can program
over it! E.g. :
A test is a list of :
class CALL_METHOD
Method
m
MkValStep[] params
class CONST
Object val
•
•
•
•
•
Producing the corresponding execution
On the fly checking
Save, reload, regress
Object pool
Pretty print, including intermediate states
Mutate
Difficult, if we are to do these directly over
Junit code.
class CREATE_TARGET_OBJECT
Constructor con
class REF
int index
MkValStep[] params
13
Simple Algorithm
Top level:



Generate (and check) N number of tests
Save violating tests
Generating a test 


Create a target object u ;  = 

Repeat until violation, or maxlegth :
choose a method m  pubmeth(C)
extend  with a call to m
check classinv and m_spec
14
Checking a step u.m ( ... )
If m_spec exists, call it instead. Catch these:
1.
1.
2.
3.
4.
PRE AssertError  discard 
Other AssertError  spec violation
Other Error or RunTimeException  internal violation
Other Exception  no violation (expected)
Check classinv on u, catch these:
2.
1.
2.
3.
APPMODEL AssertError  discard 
Other Throwable  violation + warning
Nothing thrown, but returns false  violation
15
Every step in a test, is a call m( …. )
Whatever the decision, it is represented as a MkValStep object

Create a fresh object by calling a constructor (via reflection).

Reuse a previously created object.



Also cover over side effects!
Require you to maintain a pool of objects.
T2 additionally allows you to supply a base domain:


Is searched first  can force range
Use cloning  side effect free
16
Main Testing API

Class RndEngine
static void RndTest (Pool p,
BaseDomain d,
InterfaceMap m,
Class C,
String[] options )
17
** Error trace [1] :
** CREATING target object:
(U2.T2.examples.SortedList) @ 0
s (LinkedList) @ 1
max NULL
** STEP 1.
** Calling method insert with:
** Receiver: target-obj
** Arg [0:]
(Integer) : 29
** Target object after the step:
(U2.T2.examples.SortedList) @ 0
s (LinkedList) @ 3
[0] (Integer) : 29
max (Integer) : 29
** STEP 2.
** Calling method insert with:
** Receiver: target-obj
** Arg [0:]
(Integer) : 0
** Target object after the step:
(U2.T2.examples.SortedList) @ 0
s (LinkedList) @ 5
[0] (Integer) : 0
[1] (Integer) : 29
max (Integer) : 0
** STEP 3.
** Calling method get_spec with:
** Receiver: target-obj
** Throwing java.lang.AssertionError:
POST
** Target object after the step:
(U2.T2.examples.SortedList) @ 0
s (LinkedList) @ 3
[0] (Integer) : 29
max (Integer) : 29
** Assertion VIOLATED!
** Strack trace:
java.lang.AssertionError: POST
at
U2.T2.examples.SortedList.get_spec(Sorted
List.java:44)
...
18
Programming Specifications
1.
2.
Application model
Temporal properties
Abstract View
C
Application
Automaton ANY(C).
the state is
the object pool
skip
Implicitly assume App respects C’s
ownership claim.
....
m1
m2
-step
A behavior of C is an (infinite) path in ANY.
A property is a predicate over paths.
A test is a finite prefix of a path.
....
Btw, a single threaded model !
20
Application Model
skip
....
T2 only cheks the m-steps!
m1
m2
To force T2 to check the constraint,
put it in the the classinv.
-step
....
What if we know something about App?
Model this assumption as constraints over ANY.
Don’t constrain -steps.
You can still constrain e.g. order in which methods of C are called.
21
Example
boolean classinv() {
will be filled by T2
assert appmodel() : “APPMODEL”
return …. // old spec
private String aux_laststep = null
private int aux_delta = 0
}
public boolean appmodel() {
if (aux_laststep.equals("insert"))
if (aux_laststep.equals("get"))
aux_delta++
aux_delta--
return aux_delta>=0 ;
}
22
Temporal Property


Properties are predicates over paths  so they are
all temporal.
Add it to SortedList;
change methods etc.
Example. For all M,S we require:
s == S &&



max == M
unless
open
Checking a predicate over paths implies we have to
maintain paths.
Complicated!  T2 only maintains current state.
If the the state-preds are closed in u, the prop is insensiteve!
23
Rephrase the property

Introduce aux-vars to maintain past states.

Now we can express the property as a classinv :
aux_open_frozen
|| (aux_s_frozen.equals(s) && aux_max_frozen==max)
|| open
Also extends classinv to update the aux-vars
accordingly.
24
Some Related Work
1.
2.
Verification
Other testing approaches
How is T2 related to Verification ?

Checking temporal property  essentially as in explicitstate model checking (SPIN)



JPAX : runtime verification tool




MC generates paths from models
Finite states  can generate all paths!
Generates finite paths from a real application
Obviously you can’t generate all paths; so just pick some.
v execution  fault may only surface after
Problem: no control over
a long execution
T2


generate finite paths from a real unit
Full control over thevgeneration of paths
26
Other Path-based Testing Approaches

TestLog (Ducasse et al)



Palulu (Artzi et al)



Mine paths from execution of a real application
Use Prolog to ‘query’ properties over those paths
Mine paths from execution of a real application
Use them to construct an application model
CnC


Isolated (not path-based) approach
Use a combo of Hoare-logic/theorem prover/constraint solver to
calculate tests data
27
Some Results
Class
BinarySearch
Tree
#Meth
Aver. Max.
#
Cyclo Cyclo Inst
Meth
Cov.
(%)
Block
Cov.
(%)
Time
(ms)
Fault
#step
18
2.4
7
359
100
94
907
No
20 K
7
3.6
6
212
100
98
16
yes
0.5 K
Show
13
4.4
33
844
88
84
2500
no
5K
Pool
10
2.9
7
340
100
91
531
no
5K
SortedList
Not a Swiss Knife…

Some classes are not suitable for T2. E.g. two main
classes in T2 :
RndEngine  only has one main API
Its internal behavior (e.g. loop invariant) is more interesting.
Trace  can’t generate meaningful instances on its own.
.
Class
#Meth
Aver.
Cyclo
Max.
Cyclo
#instr
Trace
14
6,3
22
1133
RndEngine
15
7,8
21
2117
Research Status


On going.
Tool  prototype, but fully functional


Paper and documentation provided
Open issues (Master thesis topics)



Is it really useful? Can it scale up?
Making the random testing more directed, e.g. by
using WP-logic
Dealing with ownership issue
Testing User Interface
Applying complementary ideas from other approaches
30
Conclusion


On-going.
S/W :





Not an all-purpose solution
Cannot handle concurrency
Strong features
Preliminary results seem promising
www.cs.uu.nl/wiki/WP/T2Framework
31