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.
What is JmlOk2?
JmlOk2 in action
The video demonstrating all JmlOk2 features is available online: http://youtu.be/9Y4izhjCfI8.
Heuristics-Based Approach for nonconformances categorization
For purposes of replication of the experiments performed in our study, we provide the version 2.0 for download.
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.
In Figures 2 to 4 we present the main screens of the JmlOk2 tool.
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.
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:
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.
Alysson Milanez [email@example.com]
Glauber Oliveira [firstname.lastname@example.org]
Manoel Ferreira [email@example.com]
Tiago Massoni [firstname.lastname@example.org]
Rohit Gheyi [email@example.com]
Bianca Lima [firstname.lastname@example.org]
Catuxe Varjão [email@example.com]
Dênnis Souza [firstname.lastname@example.org]
Igor Ataide [email@example.com]
Tiago Massoni >