Quantifiers and Comprehensions

June 22, 2010 – 6 years, 10 months ago, by eifler

Short Description

Develop a verification technique for general quantifiers and comprehensions that is suitable for automatic verification systems.

This challenge focuses on automatic program verifiers, such as ESC/Java and Boogie. These encode the proof obligations as first-order formulas that are passed to an automatic theorem prover like Simplify. In such automatic first-order provers, common inductive definitions of generalized quantifiers are not readily available.

Code

/*@ requires 0 <= from;
@ ensures a.length <= from ==> \result == 0;
@ ensures from < a.length ==>
@         \result == (a[from].startsWith("-") ? 1 : 0) + countHits(a, from+1);
@*/
/*@ pure @*/ static int countHits(String[] a, int from) {
int n = 0;
for(int i = from; i < a.length; i++) {
if(a[i].startsWith("-")) { n++; }
}
return n;
}

A method, countHits. The requires clause specifies its precondition. The use of two ensures clauses is equivalent to the conjunction of the postconditions they specify.

Specification

Long Description

It is well known that various generalized quantifiers (such as summations and products) are useful in specifications. Similarly, mathematicians have long found that set comprehensions are very convenient notational abbreviations. Haskell and other functional languages also use comprehension notations for lists to great effect.

Generalized quantifiers and comprehensions are equally useful and important in specification languages, where generalized quantifiers are notational shorthands and comprehensions act as literals for modeling types. A prominent example of the utility of comprehension notations is Z, in which, for example, set comprehensions are a central and important feature. JML has a few kinds of generalized quantifiers and set comprehensions. The example in presented above shows the use of a generalized quantifier \num_of, which counts the number of integers, j, that both satisfy the range predicate, 0 <= j && j < args.length, and the body predicate args[j].startsWith("-"). This numerical quantifier is used in a loop invariant. The loop invariant is needed to show that count is within the boundaries of the out array, which illustrates that quantifiers can be useful even in situations where one’s verification ambitions are limited, like trying only to prove the absence of array index bounds errors; of course, quantifiers and comprehensions are even more useful if one is trying to prove full functional correctness.

Quantifiers and comprehension expressions pose several pitfalls for specification language designers. For example, if quantifiers only quantify over non-garbage objects, then they become sensitive to garbage collection, which causes semantic problems. On the other hand, quantifying over non-allocated objects is also problematic. For instance, if the quantifier in the invariant of class ModelSet (Fig. 1 on page 4) ranges over all objects including non-allocated objects, then the invariant calls methods with parameter objects that are not allocated. It is unclear what it means if these methods access the state of these parameter objects. There are also practical difficulties in the implementation of quantifiers for runtime assertion checking, which require either restriction of the language or recognition of patterns of bounded quantification. Similar difficulties affect comprehension expressions. However, these difficulties in language design and runtime assertion checking seem fairly well understood.

Supplementary Materials

The paper by Gary T. Leavens and K. Rustan M. Leino and Peter Müller from which this challenge is taken contains some additional information including references to relevant papers related to this challenge. Some more specification and verification challenges which are also included on this site can also be found there.

Submitted by

Timo Eifler verifythis@cost-ic0701.org