# Assume statements (assume clauses)

## Assume statements (`assume`

clauses)

Like an `assert`

stastement, a JML `assume`

statement may be used in the
body of a method. The effect of an `assume`

statement is to instruct
the verification engine to assume, *without proof*, that the given
predicate is true. Such statements can be used to introduce
facts that are too difficult for the proof engine to prove.
They can also be used to temporarily summarize the effect of preceding code
for the purpose of attempting to prove later code; then one goes back later
to work with the preceding code until the assumption is successfully
proven and the `assume`

statement can be removed.

For example, consider the following code:

```
// openjml -esc T_assume1.java
public class T_assume1 {
//@ ensures a[\result] == 0;
public int findZeroElement(int[] a) {
int i = 0;
for (; i < a.length; i++) {
//@ assume 0 <= i < a.length;
if (a[i] == 0) break;
}
//@ assume 0 <= i < a.length && a[i] == 0;
return i;
}
}
```

Here we have stated a postcondition we want in the ensures clause and a sketch of an implementation to compute it. But we donâ€™t know yet how to specify the behavior of loops (that is coming later!), so we add some assumptions that we expect to be true. With those assumptions, the above example verifies.

Assume statements can be very helpful in developing a proof of an implementation, but they have a danger. If the given predicate is not actually
true, then it will be possible to prove invalid statements about a program.
You can even see that in the example above: if the array `a`

does not
contain any element that is zero, then the second `assume`

statement is
invalid and the postcondition cannot actually be proved.

The situation can even be worse. Consider the following drastic, if trivial, case.

```
// openjml -esc T_assume2.java
public class T_assume2 {
//@ requires i > 0;
public void example(int i) {
//@ assert false; // Blatant verification failure
}
}
```

Here we have an `assert`

statement that is explicitly false. So the verifier
will always report that the assertion is not provable and will produce
this output:

```
T_assume2.java:5: verify: The prover cannot establish an assertion (Assert) in method example
//@ assert false; // Blatant verification failure
^
1 verification failure
```

But now we add an erroneous `assume`

statement, one that contradicts the
precondition. Remember that the precondition is assumed at the start of a
method implementation and that the `assume`

statement
is also silently assumed at its location in the body.

```
// openjml -esc -checkFeasibility=none T_assume3.java
public class T_assume3 {
//@ requires i > 0;
public void example(int i) {
//@ assume i < 0;
//@ assert false; // No error because the precondition and assume statement contradict!
}
}
```

Now OpenJML issues no verification errors. The effect is just like the situation in logic where once a contradiction is assumed, anything, even false statements, can be proven.

Thus, to emphasize the point: `assume`

statements can be very helpful in the course of developing
a specification and proof of a method implementation, but they should be
replaced with `assert`

statements or removed altogether before a verification
is considered sound.