I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
jMoped 2.0 - Screenshots

The following screenshots show how jMoped can be used for testing a quicksort implementation. The plug-in is on the left-hand side under the jMoped tab. Every variable has 4 bits in this case, and the heap size is 15. Roughly speaking, the heap size determines the number of objects in the program. Then, the method sort at line 54 is right-clicked and Run As -> jMoped is chosen.

jMoped simulates the execution of sort for all possible array values inside a range. Users can indicate ranges by using Java annotations. In the example, the array has length five and each element can be only zero or one. jMoped puts green markers in front of Java statements if they are reachable from sort by some argument values. Black markers mean not reachable. The red marker at line 59 means that the assertion statement has been violated.

You can generate arguments that violate the assertion by clicking on the red marker.

A JUnit test case can be generated for further testings.