We will compare the answers collected here to results given by a semi-automated technique to categorize JML nonconformances. We thus really appreciate your time providing us those answers.
Concerning categories, a possibly missing or badly written contract is regarded as a SPECIFICATION ERROR; in contrast, a CODE ERROR is defined when the program is not fulfilling an apparently correct contract; it is UNDEFINED when it is not possible, from the context, to determine whether the problem is in the contract or in the source code.
Each of those errors may present several LIKELY CAUSES, which cannot be deterministically diagnosed - debugging can be aided, however, by specific heuristics.
In Figure 1 we present an overview of our categorization model.
Brief information about each nonconformance is provided, such as location and type. Next, we show a link to the source code of the target class (containing contracts and source code), along with a test case that reveals the nonconformance.
2. Examine the test case that shows the nonconformance, so you understand the state changes performed until the nonconformance be shown.
3. Choose an error category: code, specification, or undefined.
4. Suggest a likely cause for the nonconformance. There is a text field in which you can summarize the cause with a brief sentence. Examples: 'the precondition didn't test the parameter', or 'return variable is not correctly set'.
Source code: https://www.dropbox.com/s/d7cj5bekchcc1ja/Division.java?dl=0
Test case showing the nonconformance: https://www.dropbox.com/s/bseone66o3jeg7l/TestDivision.java?dl=0
Source code: https://www.dropbox.com/s/srlto9y0pedy0mi/Count.java?dl=0
Test case showing the nonconformance: https://www.dropbox.com/s/7dl2m2hztx151tw/TestCount.java?dl=0
Method: Constructor - Diagnostic
Source code: https://www.dropbox.com/s/vavrlz91888d844/Diagnostic.java?dl=0
Test case showing the nonconformance: https://www.dropbox.com/s/fdbyg0nke05azln/TestDiagnosis.java?dl=0