JML Tutorial - Inspecting Counterexamples
In normal operation, if openjml detects a verification failure, it simply reports information about the kind and location of the failure. But there is additional information under the hood.
The first bit of evidence to consider is the name of the assertion failure. For example a NegativeArraySize
failure indicates that an attempt was made to allocate an array, but the size given was negative. A table of all such types of verification failures is given in the OpenJML Users’ Guide.
show statement
A failed proof means that the prover found some set of input values that caused a violation of some assertion. So an easy first step is to ask for the values of relevant program variables. Consider this example:
// openjml --esc T_show1.java
public class T_show1 {
//@ ensures \result >= a && \result >= b && \result >= c && \result >= d;
//@ ensures \result == a || \result == b || \result == c || \result == d;
int max(int a, int b, int c, int d) {
int maxSoFar = a;
if (b > maxSoFar) maxSoFar = b;
if (c > maxSoFar) maxSoFar = c;
if (d > maxSoFar) maxSoFar = c;
return maxSoFar;
}
}
which produces
T_show1.java:10: verify: The prover cannot establish an assertion (Postcondition: T_show1.java:3:) in method max
return maxSoFar;
^
T_show1.java:3: verify: Associated declaration: T_show1.java:10:
//@ ensures \result >= a && \result >= b && \result >= c && \result >= d;
^
2 verification failures
So there is an error somewhere. Now if we insert a show
statement, we can see an example of values that produce the problem.
// ## openjml --esc T_show2.java
public class T_show2 {
//@ ensures \result >= a && \result >= b && \result >= c && \result >= d;
//@ ensures \result == a || \result == b || \result == c || \result == d;
int max(int a, int b, int c, int d) {
int maxSoFar = a;
if (b > maxSoFar) maxSoFar = b;
if (c > maxSoFar) maxSoFar = c;
if (d > maxSoFar) maxSoFar = b;
//@ show a, b, c, d, maxSoFar;
return maxSoFar;
}
}
which produces
T_show2.java:10: verify: Show statement expression a has value ( - 2147480361 )
//@ show a, b, c, d, maxSoFar;
^
T_show2.java:10: verify: Show statement expression b has value ( - 2147480362 )
//@ show a, b, c, d, maxSoFar;
^
T_show2.java:10: verify: Show statement expression c has value ( - 2147477363 )
//@ show a, b, c, d, maxSoFar;
^
T_show2.java:10: verify: Show statement expression d has value ( - 2147477362 )
//@ show a, b, c, d, maxSoFar;
^
T_show2.java:10: verify: Show statement expression maxSoFar has value ( - 2147480362 )
//@ show a, b, c, d, maxSoFar;
^
T_show2.java:11: verify: The prover cannot establish an assertion (Postcondition: T_show2.java:3:) in method max
return maxSoFar;
^
T_show2.java:3: verify: Associated declaration: T_show2.java:11:
//@ ensures \result >= a && \result >= b && \result >= c && \result >= d;
^
7 verification failures
The values shown are the result of a non-deterministic search; they might very well be different values on subsequent runs.
Nevertheless, for the values of a
, b
, c
, and d
shown here, the result is equal to b
or d
, instead of, for these values, the value of a
.
Some code inspection shows that there is a cut&paste error on line 9.
The counterexample is always in terms of concrete values — that is how the underlying solvers work. One would much rather have a symbolic condition that represents the cases that fail, but that is beyond the current state of the art. At present, the best one can do is do some human induction based on a few examples to understand when a program or its specification fails.
A few comments about the show
statement are in order:
- Any variable names in the
show
statement must be in scope at that position in the program. - The values are reported as of that position in the program. If we had moved the
show
statement in the above example to an earlier line, the value ofmaxSoFar
would be different. - You can include expressions in the list of items to show, not just variable names.
- However, the expressions are evaluated as specification expressions, in other words using mathematical integers (
math_mode
, cf. the discussion on Arithmetic) and so might have a different value than the same expression in Java code. - The
show
statement must be along the execution path that leads to the violation. For example, if the violation is in the then branch of an if-statement but theshow
statement is in the else branch, theshow
statement will have no effect. - Evaluation of the program stops when a violation is found. So if the
show
statement is after the line with the violation, it will not result in any output.
To illustrate the last bullet point above, consider
// openjml --esc T_show3.java
public class T_show3 {
//@ public invariant data.length >= 10;
//@ spec_public
private int[] data = new int[10];
//@ requires i >= 0;
public int data(int i) {
int r = data[i];
//@ show i, r;
return r;
}
}
which yields
T_show3.java:8: verify: The prover cannot establish an assertion (PossiblyTooLargeIndex) in method data
int r = data[i];
^
1 verification failure
There is no output from the show
statement because it is after the violation.
Instead if we put the show
statement first, as in
// openjml --esc T_show4.java
public class T_show4 {
//@ public invariant data.length >= 10;
//@ spec_public
private int[] data = new int[10];
//@ requires i >= 0;
public int data(int i) {
//@ show i, data.length;
int r = data[i];
return r;
}
}
we are told
T_show4.java:8: verify: Show statement expression i has value 1807
//@ show i, data.length;
^
T_show4.java:8: verify: Show statement expression data.length has value 1806
//@ show i, data.length;
^
T_show4.java:9: verify: The prover cannot establish an assertion (PossiblyTooLargeIndex) in method data
int r = data[i];
^
3 verification failures
\lbl expression
The show statement lets you display values of variables or of computations. But sometimes one needs to see the value of a subexpression in situ,
without recomputing it as one of the shown values. For this purpose the \lbl
expression can be used, within specifications.
For example, suppose you have a postcondition ensures a+b < c+d;
which is failing. You can label some subexpressions as follows:
ensures (\lbl AB a+b) < (\lbl CD c+d);
. The \lbl
expression just passes on its value (like a parenthesized expression), but records the value to report in
a counterexample. For example, we could try this on the example from the last subsection:
// openjml --esc T_show2a.java
public class T_show2a {
//@ ensures (\lbl A \result >= a) & (\lbl B \result >= b) & (\lbl C \result >= c) & (\lbl D \result >= d);
//@ ensures \result == a || \result == b || \result == c || \result == d;
int max(int a, int b, int c, int d) {
int maxSoFar = a;
if (b > maxSoFar) maxSoFar = b;
if (c > maxSoFar) maxSoFar = c;
if (d > maxSoFar) maxSoFar = b;
return maxSoFar;
}
}
producing
T_show2a.java:3: verify: Label A has value true
//@ ensures (\lbl A \result >= a) & (\lbl B \result >= b) & (\lbl C \result >= c) & (\lbl D \result >= d);
^
T_show2a.java:3: verify: Label B has value true
//@ ensures (\lbl A \result >= a) & (\lbl B \result >= b) & (\lbl C \result >= c) & (\lbl D \result >= d);
^
T_show2a.java:3: verify: Label C has value false
//@ ensures (\lbl A \result >= a) & (\lbl B \result >= b) & (\lbl C \result >= c) & (\lbl D \result >= d);
^
T_show2a.java:3: verify: Label D has value false
//@ ensures (\lbl A \result >= a) & (\lbl B \result >= b) & (\lbl C \result >= c) & (\lbl D \result >= d);
^
T_show2a.java:10: verify: The prover cannot establish an assertion (Postcondition: T_show2a.java:3:) in method max
return maxSoFar;
^
T_show2a.java:3: verify: Associated declaration: T_show2a.java:10:
//@ ensures (\lbl A \result >= a) & (\lbl B \result >= b) & (\lbl C \result >= c) & (\lbl D \result >= d);
^
6 verification failures
That information tells us that the problem has to do with inputs c
and d
. Note that the example changed from using short-circuiting &&
to non-short-circuiting &
and operators. Otherwise if the \result >= a
conjunct is false, that value is reported, but the rest of the precondition is not evaluated.
Though \lbl
can be used in any specification expression, it is most useful in method specifications where a show
statement cannot be placed.
ghost declarations
JML allows placing ghost declarations (discussed here) as statements in the body of a method.
They can also be useful to record values of variables and them compare them to others, show
them, perform specification-side computations, etc. as part of the debugging process.
Execution traces: the --trace
and --subexpressions
options
Using a show
statement is handy but is a bit like debugging a program using print statements: you get some data, but you have to still manually review the program to see what might be going wrong, working through the code step by step. An additional openjml tool is the --trace
option. Upon a failure, it outputs an execution trace ending at the point of the violation. So the first example above, using now openjml --esc --trace T_show1.java
, produces
T_show1.java:10: verify: The prover cannot establish an assertion (Postcondition: T_show1.java:3:) in method max
return maxSoFar;
^
T_show1.java:3: verify: Associated declaration: T_show1.java:10:
//@ ensures \result >= a && \result >= b && \result >= c && \result >= d;
^
TRACE of T_show1.max(int,int,int,int)
T_show1.java:1: requires true;
T_show1.java:6: int maxSoFar = a
T_show1.java:7: if (b > maxSoFar) ...
Condition = true
T_show1.java:7: maxSoFar = b
T_show1.java:8: if (c > maxSoFar) ...
Condition = true
T_show1.java:8: maxSoFar = c
T_show1.java:9: if (d > maxSoFar) ...
Condition = true
T_show1.java:9: maxSoFar = c
T_show1.java:10: return maxSoFar;
T_show1.java:3: ensures \result >= a && \result >= b && \result >= c && \result >= d;
T_show1.java:10: Invalid assertion (Postcondition)
: T_show1.java:3: Associated location
2 verification failures
This tells you the execution route to the violation. But more useful is the --subexpressions
option, which will give additional information.
Using openjml --esc --subexpressions T_show1.java
we get
T_show1.java:10: verify: The prover cannot establish an assertion (Postcondition: T_show1.java:3:) in method max
return maxSoFar;
^
T_show1.java:3: verify: Associated declaration: T_show1.java:10:
//@ ensures \result >= a && \result >= b && \result >= c && \result >= d;
^
TRACE of T_show1.max(int,int,int,int)
T_show1.java:1: requires true;
VALUE: true === true
T_show1.java:6: int maxSoFar = a
VALUE: a === ( - 8946 )
VALUE: maxSoFar === ( - 8946 )
T_show1.java:7: if (b > maxSoFar) ...
VALUE: b === ( - 8945 )
VALUE: maxSoFar === ( - 8946 )
VALUE: b > maxSoFar === true
VALUE: (b > maxSoFar) === true
Condition = true
T_show1.java:7: maxSoFar = b
VALUE: b === ( - 8945 )
VALUE: maxSoFar = b === ( - 8945 )
T_show1.java:8: if (c > maxSoFar) ...
VALUE: c === 1
VALUE: maxSoFar === ( - 8945 )
VALUE: c > maxSoFar === true
VALUE: (c > maxSoFar) === true
Condition = true
T_show1.java:8: maxSoFar = c
VALUE: c === 1
VALUE: maxSoFar = c === 1
T_show1.java:9: if (d > maxSoFar) ...
VALUE: d === 2
VALUE: maxSoFar === 1
VALUE: d > maxSoFar === true
VALUE: (d > maxSoFar) === true
Condition = true
T_show1.java:9: maxSoFar = c
VALUE: c === 1
VALUE: maxSoFar = c === 1
T_show1.java:10: return maxSoFar;
VALUE: maxSoFar === 1
T_show1.java:3: ensures \result >= a && \result >= b && \result >= c && \result >= d;
VALUE: \result === 1
VALUE: a === ( - 8946 )
VALUE: \result >= a === true
VALUE: \result === 1
VALUE: b === ( - 8945 )
VALUE: \result >= b === true
VALUE: \result >= a && \result >= b === true
VALUE: \result === 1
VALUE: c === 1
VALUE: \result >= c === true
VALUE: \result >= a && \result >= b && \result >= c === true
VALUE: \result === 1
VALUE: d === 2
VALUE: \result >= d === false
T_show1.java:10: Invalid assertion (Postcondition)
: T_show1.java:3: Associated location
2 verification failures
It still takes some manual inspection, but the trace of subexpression values is better than having to do that tracing oneself from the input values provided by show
.
Counterexamples
Though the subexpression option above usually provides the most useful information for debugging, it is also possible to dump all the counterexample information.
The --counterexample
or -ce
options do this. However, the output is quite verbose and (at present) uses internal encodings of variable names. Improving this information is a planned task, but at the moment the output is useful mainly to experts.