This project is read-only.

Spec# invariant question

Nov 11, 2010 at 3:46 PM

Hello,

I am not sure if this is the right place to ask, but there's not much information or other communities on spec# so I'll give it a try.

I have this code, which takes the first two elements of a fibonacci serie with length n and returns the fibonacci sequence:

public static int[]! sequenceGenerate(int n, int a, int b)
    requires n>=2;
    ensures result.Length==n;
    ensures result[0] == a && result[1] == b;
    ensures forall{int j in (2: n); result[j]==(result[j-1]+result[j-2])};
    {
        int a0=a;
        int a1=b;
        int a2=a+b;
        int[]! r=new int[n];
                r[0]=a0;
                r[1]=a1;
        int i=2;
        while(i<n)
            invariant i>=2 && i<=n;
            invariant r[0]==a;
            invariant r[1]==b;
            invariant forall{int k in (2: i); r[k]==(r[k-1]+r[k-2])};
        {
            r[i]=a2;
            a0=a1;           
            a1=a2;
            a2=a0+a1;
            i++;
        }
        return r;
    }

 

When running the verifier it says the last invariant might not hold after loop iteration. Now I have checked this many times I have no idea why this is! For example, given n=4, a=0 and b=1:

 

After 1st loop:

r[0] = 0

r[1] = 1

r[2] = 1          =      r[1]+r[0]

After 2nd loop:

r[0] = 0

r[1] = 1

r[2] = 1          =      r[1]+r[0]

r[3] = 2         =      r[2]+r[1]

 

Does anyone have a suggestion to why this is? What detail have I missed?

 

 

Nov 11, 2010 at 5:37 PM

Hi,

I believe that you need some additional loop invariants like these:

 

invariant a0 == r[i-2];
invariant a1 == r[i-1];
invariant a2 == a0 + a1;

 

If you add them, it should verify.

Is there some reason why you introduce these variables? The following code also verifies just fine:

 

public static int[]! sequenceGenerate(int n, int a, int b)
    requires n >= 2;
   ensures result.Length == n;
   ensures result[0] == a && result[1] == b;
   ensures forall{int j in (2: n); result[j] == (result[j-1] + result[j-2])};
{
   int[]! r = new int[n];
   r[0] = a;
   r[1] = b;

   for (int i = 2; i < n; i++)
      invariant 2 <= i && i <= n;
      invariant r[0] == a;
      invariant r[1] == b;
      invariant forall{int k in (2: i); r[k] == (r[k-1] + r[k-2])};
   {
      r[i] = r[i - 1] + r[i - 2];
   }
   return r;
}

 

Regards,

Valentin

 

Nov 16, 2010 at 4:11 PM

Hello,

 

Yes, that worked nicely!

 

I have another question, regarding recursive methods, such as a recursive fibonacci or similiar; how do you deal with the postcondition(ensures)? Whenever I add a recursive call as a postcondition, it wants the method to be pure, confined, etc. I've read up on the tutorials but I am unsure how to solve this.

If I add the [Pure]tag, I get a verficiation error saying "Cannot translate expression postfixexpression" on the method. What does that error mean? What do you have to do to make recursive methods verify?

 

Cheers

Nov 16, 2010 at 7:29 PM

Dear annonymous Spec# user,

Could you please post the method that exhibts the problem?

Thanks,
   Peter

Nov 16, 2010 at 7:44 PM
Edited Nov 17, 2010 at 9:19 AM

EDIT

Nov 17, 2010 at 8:38 AM

Hi,

the reason this doesn't compile seems to be that you use the postfix expression "time--" instead of "time-1".  "time--" is not side-effect free, which is why you should not use it in an assertion/contract.

If I replace both postfix expressions and make the 'bang2' method pure, the code verifies.

Regards,

Valentin

 

Nov 17, 2010 at 9:17 AM
Edited Nov 20, 2010 at 12:39 PM

The verifier works good now :) but I have a very very wierd runtime problem

using these values:

int courierA = 0;
        int courierB = 9;
        int time = 15;
        int[] locations = new int[10] {1,2,3,4,5,5,5,6,7,8};
        Console.WriteLine(bang2(locations,courierA,courierB,time));

The function should stop around time=10 or time=11 , when courierA==courierB. However, I get this:

 

Time: 15    Courier A: 0     Courier B: 9
Time: 14    Courier A: 1     Courier B: 8
Time: 13    Courier A: 2     Courier B: 7
Time: 12    Courier A: 3     Courier B: 6
Time: 11    Courier A: 4     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 11    Courier A: 4     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 12    Courier A: 3     Courier B: 6
Time: 11    Courier A: 4     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 11    Courier A: 4     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 13    Courier A: 2     Courier B: 7
Time: 12    Courier A: 3     Courier B: 6
Time: 11    Courier A: 4     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 11    Courier A: 4     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 12    Courier A: 3     Courier B: 6
Time: 11    Courier A: 4     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 11    Courier A: 4     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 14    Courier A: 1     Courier B: 8
Time: 13    Courier A: 2     Courier B: 7
Time: 12    Courier A: 3     Courier B: 6
Time: 11    Courier A: 4     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 11    Courier A: 4     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 12    Courier A: 3     Courier B: 6
Time: 11    Courier A: 4     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 11    Courier A: 4     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 13    Courier A: 2     Courier B: 7
Time: 12    Courier A: 3     Courier B: 6
Time: 11    Courier A: 4     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 11    Courier A: 4     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 12    Courier A: 3     Courier B: 6
Time: 11    Courier A: 4     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 11    Courier A: 4     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5
Time: 10    Courier A: 5     Courier B: 5

True

 

 

How on earth does that add up? The function should terminate upon courierA==courierB! Where do even these other recursive calls come from?! How can time increase? I'm not sure how this adds up

[P

[Pure]

Nov 17, 2010 at 1:30 PM

Hi,

Spec# adds runtime assertion checks in the generated code. In your case, it checks the postcondition of 'bang2' after every execution of that method. To check your last ensures clause, it needs to call the 'bang2' method recursively. Since you do IO in a pure method, this will result in additional output.

Best regards,

Valentin

 

P.S.: Since other people might also be interested in this discussion, I would be glad if you could "unedit" your previous post.

 

Nov 18, 2010 at 2:37 PM

Ah, I see. So there's nothing wrong with the code I guess, it's just the console messing.

 

Is there any way of observing the results while the method executes without this issue?