TestEra: A Tool for Testing Java Programs

Using Alloy Specifications

TestEra is a framework for specification-based testing of Java programs. To test a Java method, TestEra uses the method’s pre-condition specification to generate test inputs and the post-condition to check correctness of outputs.

Publications

TestEra: A Novel Framework for Automated Testing of Java Programs

By Darko Marinov and Sarfraz Khurshid
16th IEEE Conference on Automated Software Engineering
(ASE 2001), San Diego, CA, November 2001. [Download]

TestEra: Specification-based Testing of Java Programs Using SAT

By Sarfraz Khurshid and Darko Marinov
Automated Software Engineering Journal
(JASE 2004), 11(4):403-434, October 2004. [Download]

TestEra: A Tool for Testing Java Programs Using Alloy Specifications

By Shadi Abdul Khalek, Guowei Yang, Lingming Zhang, Darko Marinov, and Sarfraz Khurshid
26th IEEE/ACM International Conference On Automated Software Engineering, Tool Demonstrations Track
(ASE Demo 2011), Lawrence, KS, November 2011. (To appear)

Installation Steps

The TestEra distribution mainly contain two parts: the TestEra library, which provides core functionalities of TestEra and the TestEra plug-in, which is built on the TestEra library and provides friendly user interface.

Installing TestEra plug-in: The installation is quite simple, the user can install the TestEra plug-in by putting testEra-plugin_1.0.0.jar and testEra-libs_1.0.0.jar into the Eclipse plug-in directory and restart Eclipse. The user can choose from the Eclipse IDE menu: “Help”->“About Eclipse SDK”->“Installation Details”, then the installation for the TestEra plug-in is successfully done if “testEra-plugin” and “testEra-libs” appear in the “Plug-ins” tab.

TestEra Annotation

Currently, we support the following five elements of the TestEra annotation:

  1. isEnabled

    2. It instructs TestEra whether to use the annotated field or class in the translation between Java and Alloy. The default value is true. For example, the following annotation

    @TestEra(isEnabled=false) int f;

    specifies that the associated field f not be translated.

  2. invariant

    3. It applies only to classes and specifies the class invariants, which are translated into Alloy facts. For example, the following annotation

    @TestEra(invariant={"all l: LinkedList | l.size = #l.header.*next"})

    specifies the invariant on the size and the nodes of the list. Multiple invariants are strings separated by commas.

  3. preCondition

    4. It applies only to methods and specifies the constraints that the test input must satisfy before executing the method. Similar to invariants, multiple constraints are strings separated by commas. For example, the following annotation

    @TestEra(preCondition={"x >= 0"})

    specifies that the value of variable x must be non-negative.

  4. postCondition

    5. It applies only to methods and specifies the constraints that the method execution must satisfy in the post-state. The post-condition can specify a relationship between the post-state and pre-state of the method execution. For example, the following annotation

    @TestEra(postCondition={"this.size’=this.size + 1"})

    specifies that size in the post-state is the size in the prestate plus 1.

    Note that the '’' character (apostrophe) denotes field traversal in the post-state. In contrast, fields without '’' represent those in the pre-state. For non-static methods, the keyword 'this' represents the receiver object of the method under test. A post-condition can specify a constraint on the return value of the method invocation, where '\result' is used to denote the return value. For example, the following annotation

    @TestEra(postCondition={"\result=this.header.value"})

    specifies that the associated method should return the value of the header of the LinkedList.

  5. runCommand

    6. It applies only to methods and sets the scope for variables. For example, the following annotation

    @TestEra(runCommand="1 LinkedList, 3 ListNode, 3 int")

    specifies the run command scope for the variables: 1 atom for LinkedList, 3 atoms for ListNode, and 3-bit integers (-4 to 3) for the int type.

  6. limit

    7. It applies to both the method and the class levels. When applying at the class level, it specifies the maximum number of unit tests generated for each public method under the class, when applying at the method level, it specifies the maximum number of unit tests generated for the method. For example, the following annotation

    @TestEra(limit=100)

    specifies the maximum number of unit tests generated for the specified method, or each method under the specified class. Note that specifications at the method level will override specifications at the class level.

Illustrative Example

Configuring project under test: After starting the TestEra plug-in, the JUnit tests generated by TestEra need runtime access to the TestEra library. Therefore, for each project under test, the user should add the testera-lib_1.0.0.jar which includes the library as an external library through Java Build Path configuration.

Figure 1. (a) the initial source code under test, (b) the file hierarchy generated by the Alloy model generation step, (c) the file hierarchy generated by the Alloy input generation step, (d) the test hierarchy generated by the JUnit testgeneration step.

Figure 2, the pop-up menu for TestEra.

Now users can play with TestEra: Here we use a sample Java project named “sample-project”, which contains a set of data structures, for demonstration. Shown in Figure 1(a), users can right click the method under test, say linkedList.addNode(int x) here. Then the pop-up menu will have an item named TestEra (shown in Figure 2). The three sub-items of TestEra correspond to the Alloy model generation, the Alloy input generation and the JUnit test generation, respectively:

Figure 3, Alloy model generated.

  1. Alloy model generation: When the user clicks the “Generate Alloy Models” item, TestEra automatically searches all the classes referred by the method under test, and translates each compilation unit into an Alloy module under the newly created testEra-Alloy folder. The generated Alloy modules have similar file hierarchy with the source compilation units. For example, shown in Figure 1(b), the dataStructure.list.LinkedList.java compilation unit is translated into Alloy module dataStructure/list/LinkedList.als under the testEra-Alloy folder. Each generated Alloy module contains the signature definition translated from the corresponding class, as well as the class invariant extracted from the corresponding class annotation(shown in Figure 3).
    2. Figure 4, Alloy execution file generated.
  2. Alloy input generation and visualization: When the user clicks the “Visualize Alloy Inputs” item, TestEra first automatically generates an Alloy execution file for the method under test and the corresponding Alloy inputs, then invokes the Alloy visualization API to visualize the generated Alloy inputs. The generated Alloy execution file for the method under test is stored in the same directory with the Alloy model generated for its enclosing class. Figure 1(c) shows the file hierarchy of the Alloy execution file generated for method LinkedList.addNode(int x). Figure 4 shows the contents of the generated Alloy execution file, which contains both the method pre-condition specification and the run command for generating instances. Figure 5 shows the visualized Alloy input instances displayed by TestEra through invoking the Alloy’s visualization API.
    3. Figure 5, Alloy instance generated through TestEra UI.
    Figure 6, Example unit test generated.
  3. JUnit test generation: When the user clicks the “Generate JUnit Test” item, TestEra automatically generates JUnit tests for the method under test. Shown in Figure 6, the generated JUnit test contains four parts: initialization statements, pre-state abstraction, method invocation, and post-state checking. The initialization statements are concretized from Alloy inputs, the pre-state and post-state abstraction transform JUnit test inputs into abstract Alloy representations to check the correctness of the method under test using Alloy’s back-end SAT solvers. In addition, when a test passes, TESTERA provides a visualization tool that permits the user to monitor the changes between pre and post states of the input objects.

Downloads

System Requirements

TestEra library

The library is needed to run the Eclipse plugin.

TestEra Eclipse Plugin

Plugin

Examples

Please find linked list and binary search tree examples in the sample project. We plan to release more examples in future.

Please send bug reports, comments, or questions to Guowei Yang.

This material is based upon work partially supported by the National Science Foundation (NSF) under Grant Nos. CNS-0958231, CNS-0958199, CCF-0845628, CCF-0746856, IIS-0438967, and AFOSR grant FA9550-09-1-0351. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the NSF or AFOSR.