QuantifierChanges

Proposed Quantifier Changes

Daniel M. Zimmerman, August 2009

This is a proposed set of changes to JML, initially discussed on the JML mailing list in April/May 2008.

Motivation

Currently, the JML quantifiers \min and \max (hereafter, comparison quantifiers) and \sum and \product (hereafter, arithmetic quantifiers) have restrictions that prevent them from being used with some Java types and interfaces, which may cause confusion for a typical Java programmer as well as making certain kinds of specifications impossible. For instance, arithmetic quantifiers cannot be used with the BigInteger and BigDecimal numeric types. These proposed changes aim to increase the flexibility of these quantifiers.

Terminology

This proposal does not involve changes to the JML grammar, and the JML grammar for quantifiers is not reproduced here. For the sake of clarity, the following is the terminology used to discuss quantifiers and their component parts in the remainder of this proposal.

This is a typical JML quantified expression:

     (\sum int i, j; 0 <= i && i <= j && j <= 10; i * j)

\sum is the quantifier keyword (or quantifier for short); int is the bound variable type; i and j are the bound variables; 0 <= i && i <= j && j <= 10 is the range predicate; i * j is the body; and \typeof(i * j) is the body type. The type of the entire quantified expression is always the same as its body type.

Comparison Quantifier Changes

Currently, the JML Reference Manual (in section 11.4.24.2, Generalized Quantifiers - note that this is the version of the manual available on jmlspecs.org, not a current build, but the text has not changed) states that, for both comparison and numeric quantifiers, "the expression in the body must be of a built-in numeric type, such as int or double."

Comparison quantifiers need not be restricted in such a fashion. The java.lang.Comparable interface provides comparison operations (and total orderings) for much more than the numeric types (for example, java.lang.String and java.util.Date). The proposed change is to allow the body type of a comparison quantifier to be any subtype of Comparable. An example of such a comparison quantifier would be:

     (\max String s; c.contains(s); s)

Assuming that c is a java.util.Collection, the above quantified expression would evaluate to the maximum (in lexicographic order) String in c. In general, the comparison quantifiers would use the semantics of the Comparable interface to compare the objects that satisfy the range predicate. This does not change existing comparison quantifier semantics with respect to numeric types, because all standard numeric types autobox to Comparable objects.

Arithmetic Quantifier Changes

The same restriction (to built-in numeric types) can be loosened on arithmetic quantifiers as well. The proposed change is to allow the java.math.BigDecimal and java.math.BigInteger types, as well as the JML \bigint and \real types, to be used as the body types of arithmetic quantifiers. It is possible to extend this to any subtype of java.lang.Number, but at the potential cost of numeric precision, as the only (guaranteed) way to get the value of a java.lang.Number is to convert it to a byte, double, float, int, long, or short. While this might be useful for some applications, it would likely require a change to the grammar (to explicitly indicate which conversion should be done, and thus control how much precision is lost), and is not being proposed at this time.

Other Changes

With the advent of autoboxing, all 6 of the Java primitive numeric types have corresponding object types. It would likely be useful (for runtime assertion checking purposes) to "autobox" the JML \bigint and \real types to java.math.BigInteger and java.math.BigDecimal, respectively. This would allow them to be used with comparison quantifiers as well as arithmetic quantifiers.

Empty Ranges

The question of how to deal with empty quantifier ranges (unsatisfiable range predicates) is currently resolved in the JML Reference Manual as follows:

When the range predicate is not satisfiable, the sum is 0 and the product is 1... When the range predicate is not satisfiable for \max the result is the smallest number with the type of the expression in the body; for floating point numbers, negative infinity is used. Similarly, when the range predicate is not satisfiable for \min, the result is the largest number with the type of the expression in the body.

This resolution is straightforward and uncontroversial for the numeric quantifiers, even with the introduction of the new numeric types described above. However, it is problematic for the comparison quantifiers when generalized to arbitrary Comparable body types: some body types may not have maximum or minimum elements. For instance, the minimum String is "" (the empty string), but there is no maximum String (though there is, in any given virtual machine, a maximum representable String limited by available heap space). There are several possible ways to resolve this issue, but the most straightforward, and the one proposed here, is to consider the value of any comparison quantifier with an unsatisfiable range predicate to be undefined. Further discussion may be needed on this proposed change.