JmlOk2
A tool for detect and categorize nonconformances in Contract-Based Programs
What is JmlOk2?
JmlOk2 is a tool that detects nonconformances between Java code and JML specification through the feedback-directed random tests generation.
Also, JmlOk2 is a tool that suggests likely causes for nonconformances.
JmlOk2 in action
The video demonstrating all JmlOk2 features is available online: http://youtu.be/9Y4izhjCfI8.
Download
For purposes of replication of the experiments performed in our study, we provide the version 2.0 for download.
JmlOk2 is an open source software that can available and changed by the terms of GNU (GNU General Public License) GPL v3. Currently, this tool is avaliable for Windows, Linux, and Mac Operating Systems.
Heuristics-Based Approach for nonconformances categorization
We use a heuristics-based approach for categorize nonconformances. Each heuristic is based on the type of the nonconformance. All details about this model are available here.
JmlOk2 Steps
JmlOk2 follows these steps to detect and categorize nonconformances in contract-based programs:
1- The code of the program is compiled.
2- Tests are generated with the compiled code in step 1.
3- Oracles are produced from contracts.
4- Tests generated in step 2 are run against oracles produced in step 3.
5- A filter distinguishes from all failures which distinct nonconformances were detected.
6- A subset of heuristics to each nonconformance is selected based on its type.
7- Each subset is used together the source code to choose a likely cause for the nonconformance. And finally, all detect and categorized nonconformances are returned.
The steps are shown in Figure 1.
Figure 1. Steps performed in our tool.
JmlOk2 GUI
In Figures 2 to 4 we present the main screens of the JmlOk2 tool.
Figure 2. The initial screen of the tool. In this screen the user can give the inputs needed to use the tool. If no input is given, a message dialog warns the user about the needed of at least the contract-based program to be given as input.
Figure 3. The screen resultant of Detection phase. In order to get the results of the categorization, the user have to press the button Nonconformances.
Figure 4. Categorization screen presenting the results of JMLOK 2.0 tool. For each nonconformance are presented: the type, the complete location (including information of package, class, and method), the suggested likely cause, and the test case with highlight in the line that reveals the nonconformance.
Experiments
We use our tool to evaluate some example programs, named Samples, available at: http://www.eecs.ucf.edu/~leavens/JML/examples.shtml#Samples and a set of Real programs available at literature: Bank, Bomber, Dnivra-Jive, HealthCard, JAccounting, Javacard, Mondex, PayCard, PokerTop, TheSchorrWaiteAlgorithm, and TransactedMemory; totalizing more of 26 KLOC and 4 K JML contract clauses (KJCC).
We detected 119 nonconformances, 18 in Samples and 101 in Real Programs:
For more details see:
Publications
MILANEZ, A.; SOUSA, D.; MASSONI, T.; GHEYI, R.. JMLOK2: A tool for detecting and categorizing nonconformances. In: Tools Session of the Brazilian Conference on Software: Theory and Practice, 2014.
VARJÃO, C.; GHEYI, R.; MASSONI, T.; SOARES, G. JMLok: Uma Ferramenta para Verificar Conformidade em Programas Java/JML. In: Tools Session of the Brazilian Conference on Software: Theory and Practice, 2011.
People Involved
Alysson Milanez [alyssonfilgueira@copin.ufcg.edu.br]
Manoel Ferreira [jose.ferreira@ccc.ufcg.edu.br]
Tiago Massoni [massoni@dsc.ufcg.edu.br]
Rohit Gheyi [rohit@dsc.ufcg.edu.br]
Past members
Bianca Lima [bianca.lima@ccc.ufcg.edu.br]
Catuxe Varjão [catuxe@copin.ufcg.edu.br]
Dênnis Souza [dennis.souza@ccc.ufcg.edu.br]
Igor Ataide [igor.ataide@ccc.ufcg.edu.br]
Glauber Oliveira [jose.oliveira@ccc.ufcg.edu.br]