Best way to count specific elements in array / verification time depends on bound for quantified domain

Apr 8, 2014 at 12:30 PM
Hi all,
I have a program, where I count all elements of an array a, which are equal to a number i upto a specific bound. Afterwards, I want to find out, which value i had the highest occurrence.
Thereby, I noticed some strange behaviour of VCC or Z3. My precondition sets a bound B for the elements to be counted. Interestingly, this bound seems to have a high effect on the performance of the proof in VCC.
I attached a minimal example of my program. The use of ghost code is simply for performance reasons, since I want to examine only the abstract implementation and no concurrency is involved.
#include <vcc.h>

_(ghost _(pure) \integer count(int a[int], int upto, int i)
        _(requires 0 <= upto && 0 < i && i <= 2)
        _(returns (upto <= 0) ?  0 : count(a, upto-1, i) + (a[upto-1] == i ?  1 :  0));)

void main(int B _(ghost int a[int]))
    _(requires \forall int i; (0 <= i && i < B ==> 0 < a[i] && a[i] <= 2))
    _(requires 0 < B && B < 80)
{
    _(ghost int b[int];)
    _(assume \forall int k; (0 < k && k <= 2 ==> (b[k] == count(a, B, k))))

    _(ghost int max = 0;)
    _(ghost for (int i = 1; i <= 2; i++)
        _(invariant \forall int k; 0 < k && k < i ==> b[k] <= max)
    {
        if (max <= b[i]) {
            max = b[i];
        }
    })
}
So, I got two questions:
  1. Is there a better way to do the counting? I already examined the solutions for the VSTTE competition (when summing up all array elements), where you used different means (e.g. a map keeping track of all counting steps) to do this, but it did not seem to help in my case.
  2. Why does the proof performance depend on a bound for a quantified domain or furthermore, how do I remove this dependency? Before shrinking down my example, the loop also contained the following invariant
_(invariant \forall int j; 0 <= j && j < B ==> b[a[j]] != 0)
which did also depend on the given bound. Is also experimented a bit using different hints and triggers, but could not get rid of the dependency yet. Does anybody have any explanations or suggestions for this matter?

I am thankful for any responses and help!