Comprehension in the loop invariant

Aug 30, 2012 at 9:45 AM

Hello,

I am studying spec# tool and got the following problem. Code below seems fine but the prover cannot see the loop invariant holds. It claims initially and after loop iteration the invariant fails.

Do I miss something?

public class Test {

	void test(int[] t) 
		requires t != null;
	{
	    int i = 0;	    
	    while(i<t.Length)
	    	invariant count {int k in (0: i); t[k] > 0} <= count {int k in (0: t.Length); t[k] > 0}; 
	    {
	    	i++;		
	    }
	}
}

Thank you,

Boriss

 

Coordinator
Aug 30, 2012 at 7:09 PM

Evidently, the Spec# verifier does not have the "obvious" information that a "count" comprehension always returns a non-negative value.  That's a pity.  If you give it that information (in the form of an assumption before the loop and at the end of the loop, in both cases for the range (i: a.Length)), then the Spec# verifier proves the program.

public class Test {
  void test(int[] t) 
    requires t != null;
  {
    int i = 0;
    assume 0 <= count {int k in (i: t.Length); t[k] > 0};
    while(i<t.Length)
      invariant count {int k in (0: i); t[k] > 0} <= count {int k in (0: t.Length); t[k] > 0}; 
    {
      i++;		
      assume 0 <= count {int k in (i: t.Length); t[k] > 0};
    }
  }
}

  Rustan

Sep 12, 2012 at 10:19 AM
Edited Sep 12, 2012 at 10:19 AM

Thank you for the reply!

I am proceeding with this but got a different problem. Now verifier proves the first assertion inside the loop body, but fails to prove the second one. 

 

public class Test {

	void test2(int[] t) 
		requires t != null;
	{
	    int i = 0;
	    assume 0 <= count {int k in (i: t.Length); t[k] > 0};	    
	    while(i<t.Length)
	    	invariant count {int k in (0: i); t[k] > 0} <= count {int k in (0: t.Length); t[k] > 0}; 
	    {
	    	assert i + 1 <= t.Length;	    	
	    	assert count {int k in (0: i+1); t[k] > 0} <= count {int k in (0: t.Length); t[k] > 0};
	    	i++;
	    	assume 0 <= count {int k in (i: t.Length); t[k] > 0};
	    }
	}

}

Boriss

 

Coordinator
Sep 12, 2012 at 7:26 PM

The property that Spec# unfortunately does not know is that count always returns a non-negative value.  So the property you need to assume is:

  assume 0 <= count { int k in (i+1: t.Length); t[k] > 0 };

Since you need this property several times, you can make it into a "lemma"--that is, the postcondition of a method that you will call when you need the property.

    void Lemma(int[] t, int start, int end)
      requires t != null && 0 <= start && start <= end && end <= t.Length;
      ensures 0 <= count { int k in (start: end); t[k] > 0 };

In fact, it is actually possible to prove this property in Spec#, which you can do by supplying a body for Lemma that convinces the verifier that the postcondition will hold.  This way, you don't need any assume statement in your program.  (However, note that Spec# does not prove termination, so if you give a non-terminating body for Lemma, you still have not really verified the lemma.)

Finally, you don't want to have the Lemma method be part of the executing code, so you can mark it for conditional compilation using the System.Diagnostics.Conditional attribute.  Here's the final program:

public class Test {

    void test2(int[] t) 
        requires t != null;
    {
        int i = 0;
        Lemma(t, i, t.Length);  // needed to establish that the invariant holds initially
        while(i<t.Length)
            invariant count {int k in (0: i); t[k] > 0} <= count {int k in (0: t.Length); t[k] > 0}; 
        {
            Lemma(t, i+1, t.Length);  // needed if you want to prove the next assertion            
            assert count {int k in (0: i+1); t[k] > 0} <= count {int k in (0: t.Length); t[k] > 0};
            i++;
            Lemma(t, i, t.Length);  // needed to show that the invariant is maintained
        }
    }

    [System.Diagnostics.Conditional("VerificationOnly")]
    void Lemma(int[] t, int start, int end)
        requires t != null && 0 <= start && start <= end && end <= t.Length;
        ensures 0 <= count { int k in (start: end); t[k] > 0 };
    {
        // This is something that, unfortunately, Spec# does not automatically know.
        if (start != end) {
            Lemma(t, start+1, end);
        }
    }
}

  Rustan

PS.  Since I work with Dafny these days, I couldn't resist writing your example in Dafny.  Dafny does not have a built-in "count" comprehension, so you have to code your own.  But Dafny has support for termination checking and verification-only compilation ("ghost" constructs), as well as an automatic induction tactic.  With these, you can write the analogous program in Dafny as follows (see also http://rise4fun.com/Dafny/AwcY7, where you can click the "try Dafny" button to verify it):

function CountPositive(t: array, start: int, end: int): nat
  requires t != null && 0 <= start <= end <= t.Length;
  reads t;
  decreases end;
{
  if start == end then 0 else CountPositive(t, start, end-1) + if t[end-1] > 0 then 1 else 0
}

method test2(t: array) 
  requires t != null;
{
  var i := 0;
  while (i < t.Length)
    invariant i <= t.Length;
    invariant CountPositive(t, 0, i) <= CountPositive(t, 0, t.Length);
  {
    Lemma(t, 0, i+1, t.Length);
    assert CountPositive(t, 0, i+1) <= CountPositive(t, 0, t.Length);
    i := i + 1;
  }
}

ghost method Lemma(t: array, i: int, j: int, k: int)
  requires t != null && 0 <= i <= j <= k <= t.Length;
  ensures CountPositive(t, i, j) + CountPositive(t, j, k) == CountPositive(t, i, k);
{
}