defaults and spec inference and standards

[davidcok]

I'd like a bit of discussion on how spec inference by tools should fit with standard JML

1) On one hand, specifications written in JML should have one clear meaning, ideally implemented with the same meaning in every tool. That would mean that the defaults are defined and fixed also.

2) On the other hand, inferred specs will make specification life easier for the user, and is a direction in which research would be appropriate. But tools are not likely to infer the same specs or do inference in the same contexts.

3) Of course, tools can always turn on inference with an execution option. But to the extent that that option becomes the standard operating procedure for using that tool, because it makes specification & verification easier, different tools will end up having different effective interpretations of the explicitly written JML.

4) One partial mitigation is that tools could say what specs they infer, so that those specs can be inserted explicitly.

Thoughts on this?

[leavens]

Thanks. I agree with point (1). I had always thought of inference of specification tools as exporting the inferred specifications in JML annotations, as in (4). I generally agree with point (2) in that different tools for JML might infer different specifications (this will be doubly true if the inference is a research project).

Inferring loop invariants and method contracts (pre- and postconditions as well as frame conditions) is probably the most important area of research on this topic. There has been some research on the (unsolvable) problem of inferring loop invariants, and we are trying to use some of that work (notably a tool called "Rapid") in a work done by Kohei Koja at UCF. However, loop invariants are needed for inference of method contracts from code that contains loops and conversely method contracts are often useful in determining what a loop invariant should look like (in practice), so the two are not completely independent.

For method contracts the issue of what is intended (by a human) and what the code does is more critical, as one would ideally like for the method contract to be stable and an agreed-on interface for the method. Also, if the method contract is inferred from the code, then the code will be verifiable against the contract, even if the contract were not exactly what a person would want; for example, the inferred contract might be more complex due to a code bug in an edge case. Ideally the contract for a method would also agree in some sense with the method's name and any (natural language) comments given by the author, but that is more of an AI question.

[mattulbrich]

Quick answer: I like (4). Perhaps the specifications are not necessarily exported into the code, but a) that should be possible and b) at least a very explicit listing should be provided. In IntelliJ etc. they show you the type of inferred type contexts explicitly. That sort of thing for inferred specifications.

[leavens]

I also like having a tool output the inferred specifications into a .jml file or other output that could be put into the code.