## Quantiﬁers and Comprehensions

*June 22, 2010 – 6 years, 9 months ago, by eifler*

### Short Description

Develop a veriﬁcation technique for general quantiﬁers and comprehensions that is suitable for automatic veriﬁcation systems.

This challenge focuses on automatic program veriﬁers, such as ESC/Java and Boogie. These encode the proof obligations as ﬁrst-order formulas that are passed to an automatic theorem prover like Simplify. In such automatic ﬁrst-order provers, common inductive deﬁnitions of generalized quantiﬁers 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 speciﬁes 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 quantiﬁers (such as summations and products) are useful in speciﬁcations. 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 quantiﬁers and comprehensions are equally useful and important in speciﬁcation languages, where generalized quantiﬁers 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 quantiﬁers and set comprehensions. The example in presented above shows the use of a generalized quantiﬁer \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 quantiﬁer 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 quantiﬁers can be useful even in situations where one’s veriﬁcation ambitions are limited, like trying only to prove the absence of array index bounds errors; of course, quantiﬁers and comprehensions are even more useful if one is trying to prove full functional correctness.

Quantiﬁers and comprehension expressions pose several pitfalls for speciﬁcation language designers. For example, if quantiﬁers 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 quantiﬁer 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 difﬁculties in the implementation of quantiﬁers for runtime assertion checking, which require either restriction of the language or recognition of patterns of bounded quantiﬁcation. Similar difﬁculties affect comprehension expressions. However, these difﬁculties 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