The lessons on assert and assume (as well as coming lessons on preconditions and postconditions) all show examples of expressions used in JML specifications. As expressions are a building block for nearly all other JML constructs, we include lessons here to introduce JML expressions.

JML expressions look very much like Java expressions. Indeed, the JML expression syntax includes all of the Java expression syntax, with this exception: JML expressions are not allowed to have effects (that is, they may not change the program’s state). So the ++, --, and op= (e.g., +=) operators are not allowed in JML expressions. The meaning of other Java operators in JML is unchanged, except for two kinds of additional checks that JML makes, which are discussed in later lessons:

Note that the non-short-circuiting boolean operators & and | are legal in both Java and JML, though the short-circuiting versions && and || are much more commonly used in Java because they can be more efficient (at runtime). In static reasoning, however, & and | are often simpler for OpenJML to reason about, but && and || are often still needed due to well-definedness considerations.

JML also adds to Java some operators and some expression syntax. The new operators are these:

  • ==> (implication): this binary operator takes two boolean operands, e.g., p and q; p ==> q is read as “p implies q” and means the same as logical implication, that is, the same as “not p or q”. The implication operator is short-circuiting. That is, the value and well-definedness of the right-hand-side is not evaluated, unless the left-hand-side is true. In other words, p ==> q is precisely equivalent to !p || q. The implication operator has lower precedence than && and ||, so p && q ==> r || s means (p && q) ==> (r || s). ==> is right associative, so that p ==> q ==> r means p ==> (q ==> r), which is the same as (p && q) ==> r.

  • <==> (equivalence): this is also a binary operation between boolean values. p <==> q means the same as p == q, except that <==> has lower precedence than && and || and ==>, whereas == has higher precedence. Thus p && q == r || s means (p && (q == r)) || s, whereas p && q <==> r || s means (p && q) <==> (r || s). Also <==> is left associative, so p <==> q <==>r means (p <==> q) <==> r), though: (a) the meaning is the same as if it were right associative and (b) expressions that rely on associativity of <==> may be confusing and so perhaps should be avoided.

  • <=!=> (inequivalence): this operator is simply the negation of <==> and has the same precedence as <==>. The operator <=!=> is also left associative; that is, p <=!=> q <==> r means (p <=!=> q) <==> r, though again, expressions relying on associativity of <=!=> and <==> may be confusing and so perhaps should be avoided.

Another important addition to JML is the chaining of relational operators. That is, instead of writing i <= j && j < k, one can write i <= j < k. Similarly, i > j > k means i > j & j > k. The operators < and <= can each be chained together, as can the operators > and >=. However, the two groups cannot be mixed, so combinations involving both < and> are illegal; for example a <= b >= c is illegal in JML. Furthermore, == does not chain and in fact has a lower precedence than the relational operators; thus a < b == c < d means (a < b) == (c < d) in both Java and JML. On the other hand, chained operations are particularly convenient for writing ranges of indices; as an example, one might constrain the index i into an array arr by writing 0 <= i < arr.length.

In addition quantified expressions are described below and two other advanced operators are presented separately in advanced topics lessons:

Finally, there are many keywords that designate either singleton values (e.g., \result) or function-like operations (e.g., \typeof(...)). These will be explained as needed in future lessons. All JML keywords used within expressions begin with a backslash, so they do not conflict with Java identifiers. For example the expression 0 <= \result < ary.length says that the result of the current method (named \result) is a legal index into the array ary.

Of course, these JML operators and functions (and all other JML syntax) can only be used within JML annotations, not in Java code.

Quantified expressions

A general point about all of the quantified expressions in JML is that their numeric subexpressions are evaluated mathematically (i.e., in bigint-math mode), so that there is no concern about overflow in evaluating the expression. Furthermore, arithmetic mode operators (that change the mode of a subexpression) are not allowed within a quantified expression; however the overall result of a quantified expression may be cast to a desired type, since that cast will operate after the mathematical value of the quantified expression is known.

forall and exists

Quantified expressions are common in logic (and are just as necessary in JML) to express properties over collections of objects. The two most common quantified expressions are universal and existential quantification. The following are some common examples involving arrays:

  • (\forall int i; 0 <= i < a.length; a[i] == 2*i)
  • (\exists int i; 0 <= i < a.length; a[i] == 0)

The first expression states the property that each (that is, all) of the elements of array a have a value equal to twice that element’s index. The second states that for some index within the array, the value at that index equals 0. Both of these expressions have the same general form: the keyword, a variable declaration (which is local to the expression), a boolean range predicate R, and a boolean value predicate V. The meaning of the range expression R in these forms is as if the quantifier had been written as shown below:

  • (\forall ...; R; V) is the same as (\forall ...;; R ==> V)
  • (\exists ...; R; V) is the same as (exists ...;; R && V)

However separating R and V makes it easier to have an efficient implementation for runtime-assertion-checking. Note that if the range predicate is false (for example if the array a has length 0 in (\forall int i; 0 <= i < a.length; V), then, as in logic, a forall expression will be true, but an exists expression with an empty range, such as (\exists int i; 0 <= i < a.length; V) will be false (with a has length 0).

The scope of the declared variable in a quantified expression extends as far to the right as possible. Thus, it is good practice, and avoids possible confusion about the scope of the declared variable, if one puts parentheses around the entire quantified expression; however, such parentheses are not required by JML.

Quantified expressions are commonly used in reasoning about loops, arrays, sequences and sets. For example, to say that every element e of a set s (where the elements have type T) has the property P(e) one could write the following expression: (\forall T e; e \in s; P(e)).

choose

The \choose quantifier is similar to \exists. Whereas (\exists T i; R; V) is true if there is some value of the quantified variable (i) for which R && V is true, (\choose T i; R; V) returns some value of i that makes R && V true (as the value of the choose expression). For example, the value of (\choose int i; 0 <= i < a.length; a[i] == 0) is some int for which the range predicate is true; in this example, that is a legal index (i) of array a holding the element 0. The type of the expression is always the type of the declared local variable (i in the example).

If there is more than one such value (in our example, more than one such index i), then the result of the expression might be any one of them, but it will always the same one for a semantically identical expression. But the fact that the value could be any one satisfying the predicate means that an assertion that uses that value must hold for all cases in which the predicate is true. For example in the expression P(\choose int i; 0 <= i < a.length; a[i] == 0), the value of the overall expression should not depend on the value chosen.

If R is false, (in our example, if there is no index i such that 0 <= i < a.length), then the expression is not well-defined. Thus, to make sure that a \choose predicate is always well-defined, one should make sure that the range expression is never false.

max and min

The \max and \min quantifiers have the same form as the quantified expressions above, except that the value term must be numeric, so that the concepts of “maximum” and “minimum” are meaningful. You might ask, for example, for the maximum and minimum values of an array:

  • (\max int i; 0 <= i < a.length; a[i])
  • (\min int i; 0 <= i < a.length; a[i])

The implementation of these two expressions in OpenJML is in progress. Don’t count on them working yet.

As a shorthand notation

A first point to note is that these min and max quantified expressions are each equivalent to a choose expression with a pair of forall and exists subexpressions inside. That is, x == (\max ...; R; v) where x has a numeric type T, is equivalent to (\choose T v; (\exists T x; R; x == v); (\forall T x; R; x <= v)). That is, the value of the \max expression is one of the elements being considered and is at least as large as all of them. Similarly, the value of x == (\min ...; R; v) is equivalent to (\choose T v; (\exists T x ; R; x == v); (\forall T x ; R; v <= x)), where T is again the type of x. That is, the value of the \min expression is a number that is one of the elements being considered and is no bigger than all of them. These equivalences are used in the example below.

    //@ spec_pure
    public int minOfPosArray (int[] a) {
        //@ assume 0 < a.length;
        //@ assume (\forall int i; 0 <= i < a.length; 0 < a[i]);
        int val = a[0];
        int k;
        for (k = 0; k < a.length; k++) {
            //@ assume 0 <= k < a.length;
            if (a[k] < val) {
                val = a[k];
            }
        }
        //@ assume k == a.length;
        //@ assume (\forall int m; 0 <= m < k; val <= a[m]);
        //@ assume (\exists int n; 0 <= n < a.length; val == a[n]);
        //@ assert val == (\min int m; 0 <= m < a.length; a[m]);
        return val;
    }

    //@ spec_pure
    public int maxOfPosArray (int[] a) {
        //@ assume 0 < a.length;
        //@ assume (\forall int i; 0 <= i < a.length; 0 < a[i]);
        int val = a[0];
        int k;
        for (k = 0; k < a.length; k++) {
            //@ assume 0 <= k < a.length;
            if (val < a[k]) {
                val = a[k];
            }
        }
        //@ assume k == a.length;
        //@ assume (\forall int m; 0 <= m < k; a[m] <= val);
        //@ assume (\exists int n; 0 <= n < a.length; val == a[n]);
        //@ assert val == (\max int m; 0 <= m < a.length; a[m]);
        return val;
    }
Well-definedness

A second point is that the quantified expression (\min T x; R; V) and (\max T x; R; V) are not well-defined if the range is empty (that is, when the range predicate, R, is false).

Type and arithmetic mode

A third point is that the type of a quantified expression (\min T x; R; V) or (\max T x; R; V) is the same as the type of the value term (V). However the value term itself is evaluated mathematically (in bigint-math mode), although the result can be cast to another type if desired.

sum and product

The \sum and \product quantifiers add up or multiply together all the values of the value term for which the range term is true. For example, the sum and product of all the elements in an array a could be expressed as:

  • (\sum int i; 0 <= i < a.length; a[i]) and
  • (\product int i; 0 <= i < a.length; a[i])

The type of these expressions is a mathematical type (that is, if integer-valued it is evaluated in bigint-math mode), because overflow is a distinct possibility. However, the result could always be cast to a desired final type.

If the range predicate is empty (i.e., false) then the sum is 0 and the product is 1. So these expressions are well-defined even when the range predicate is empty.

The implementation of these two expressions in OpenJML is in progress. Don’t count on them working yet.

num_of

A final quantified expression is \num_of which counts the number of times the boolean value term is true when the range term is also true. For example, (\numof int i; 0 <= i < a.length; a[i] == 0) counts the number of elements of the array a that are 0. The expression (\num_of ...; R; V) is equivalent to (\sum ... ; R && V; 1). Thus the type of a \num_of expression is \bigint. If the range is empty, then the value of the expression is 0.

The implementation of this expression in OpenJML is in progress. Don’t count on it working yet.

TODO - what about \let?

Exercises

Follow the link in the above heading to work on the exercises on this topic.

Resources