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.
By Darko Marinov
and Sarfraz Khurshid
16th IEEE Conference on Automated Software Engineering
(ASE 2001), San Diego, CA, November 2001. [Download]
By Sarfraz Khurshid
and Darko Marinov
Automated Software Engineering Journal
(JASE 2004), 11(4):403-434, October 2004. [Download]
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)
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.
Currently, we support the following five elements of the TestEra annotation:
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.
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.
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.
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 '
@TestEra(postCondition={"\result=this.header.value"})
specifies that the associated method should return the value of the header of the LinkedList.
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.
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.
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. |
![]() |
Figure 4, Alloy execution file generated. |
![]() |
Figure 5, Alloy instance generated through TestEra UI. |
![]() |
Figure 6, Example unit test generated. |
The library is needed to run the Eclipse plugin.
Please find linked list and binary search tree examples in the sample project. We plan to release more examples in future.