Manually categorizing nonconformances in JML programs
This form was created to evaluate a categorization model proposed and implemented for Java/JML programs.

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.

The Categorization Model
In our study we proposed and implemented a categorization model to nonconformances between code and specification. The model is composed by three-levels: category, type and likely cause.

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.

Figure 1. Categorization model - overview
Evaluation
Now we present three nonconformances - randomly selected from confirmed nonconformances detected in several JML projects.

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.

Suggested Guidelines
1. Examine the source code and contract.

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'.

Nonconformance 1
Class: Division

Method: division

Type: Precondition

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

Category
Chooses the most suitable category to this nonconformance
Likely cause
Suggests a likely cause for this nonconformance
Your answer
Nonconformance 2
Class: Count

Method: getName

Type: Postcondition

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

Category
Chooses the most suitable category to this nonconformance
Likely cause
Suggests a likely cause for this nonconformance
Your answer
Nonconformance 3
Class: Diagnostic

Method: Constructor - Diagnostic

Type: Invariant

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

Category
Chooses the most suitable category to this nonconformance
Likely cause
Suggests a likely cause for this nonconformance
Your answer
Submit
Never submit passwords through Google Forms.
This content is neither created nor endorsed by Google. Report Abuse - Terms of Service - Additional Terms