On JML Method-Level Specification Comprehension

This README file accompanies the SoSym submission titled

"On JML Method-Level Specification Comprehension"

The contents of the directory are as follows:

1. github_crawler.py and calculate_jml_stats.py - scripts used to mine the preliminary JML dataset, and to calculate the token frequencies

2. Consent.pdf and Instructions.pdf - the corresponding texts from the experiment website

3. dataset - a directory with the original Java methods and corresponding JML specifications used in our experiment, classified into folders according to the type the methods operate on and the return value.

4. frontend - a directory with *.jsx files (HTML and JavaScript code) that form together the experiment web interface

5. backend - a directory with the backend python code, consisting of:

5.1. specs - a folder organized into two subfolders: with_rewrite and without_rewrite. Contains the source code of the input/output pair generators for each specification. The files in with_rewrite folder contain the texts of the original and the rewritten JML specifications as used in the experiment, and the files in without_rewrite contain only the original JML specification texts

5.2. generator_validator.py - script to simulate executions of each pair generator and validate that the correct to incorrect pair ratio is 1:1

5.3. server.py - the Flask server-side script that generates test instances and performs the statistical analyses

5.4. Spec.py - contains code of the Spec class, from which all pair generators in the specs folder inherit

5.5. verify_specs.py - script to verify using OpenJML the correctness of the JML specifications against the corresponding Java code

6. raw_data.json - recorded response log during the execution of the experiment

7. experiment_numbers.json - general data regarding the experiment execution

8. spec_ranking.json - the full list of specifications ranked according to the comprehension difficulty score

9. rq1_regression.json - regression model analysis for RQ1 including corrected p-values

10. rq2+3+4.json - permutatation tests analysis for RQ2, RQ3, and RQ4 including corrected p-values