Hi,

I am doing some experimentation with sscBoogie. I use it to verify one of the Spec# examples that counts non-null values in an array (code below). I introduced an error in the loop boundaries; the correct version is  for (int i = 0; i < a.Length; i++).

When verifying the program, sscBoogie fails to generate an array bound error. The erroneous code also violates the invariant which should produce an error. If I remove the invariants, sscBoogie detects the error! Any ideas why this is happening?

Thanks,

Iman

----------------------------------------------------------------------------------------------------------------------

public void CountNonNull()
  {
     expose(this){
      int ct = 0;
      for (int i = 0; i > a.Length; i++)  // This is an erroneous loop!
      invariant i <= a.Length; //infers 0<=i
      invariant 0 <= ct && ct <= i; //needed to help verify next //invariant
      invariant ct == count{int j in (0: i); (a[j]!=null)};
      {
        if (a[i]!=null) ct++;
      }
      count = ct;
    }
  }

Your program text given here contains no array bounds error, so SscBoogie is correct is not issuing any complaint.  The loop variable i is initialized to 0, which is not greater than a.Length for any array a.  Thus, SscBoogie knows that control will never flow into the loop.  It will check that the loop invariant holds initially (which it does) and will then procede to consider control flow after the loop exit.

That makes total sense that there will be no array bound violation since the control will never flow into the loop. But, why does it generate an error " Array index possibly above upper bound" when the invariant is removed?

Thank you for your response!

Iman

The way the verifier handles loops is that it checks that the loop invariant (which may be just "true") holds initially.  Then, it shakes up the state of the program in a way that satisfies the (enclosing method's modifies clause and the) loop's invariant; from that state, it continues execution by evaluating the loop guard and branching accordingly.  If it gets to the end of a loop iteration, it checks that the loop invariant holds there as well.  So, for the program above, if you don't supply a loop invariant, the verifier will change i to an arbitrary value and will then check the loop guard.  In particular, it will consider the possibility that an iteration will start with a value of i that exceeds a.Length.

For more information, there are a number of texts you could read, including section 1.3 of the Spec# tutorial (http://research.microsoft.com/en-us/um/people/leino/papers/krml189.pdf) and page 6 of the lecture notes "A verifying compiler for a multi-threaded object-oriented language" (http://research.microsoft.com/en-us/um/people/leino/papers/krml168.pdf).