Problem with Loop Invariants

May 12, 2010 at 7:04 PM
Edited May 12, 2010 at 7:18 PM

Apologies in advance for the ingorant question.

I tried out Rustan's tutorial example on invariants, and tried to check the following

    void testOne(int[] a)
    modifies a[*];
    ensures forall {int i in (0: a.Length); a[i] == i*i*i};
    {
       int n=0;
       while (n<a.Length)
       invariant forall {int i in(0:n); a[i]==i*i*i};
       {
         a[n]=n*n*n;
         n = n+1;
       }
    }

But got a warning:

         Warning 1 After loop iteration: Loop invariant might not hold: forall {int i in(0:n); a[i]==i*i*i} ...

On the other hand, the following loop does verify 

    void testTwo(int[] a) 
    modifies a[*];
    ensures forall {int i in (0: a.Length); a[i] == 2*i};
    {
       int n=0;
       while (n<a.Length)
       invariant forall {int i in(0:n); a[i]==2*i};
       { 
         a[n]=2*n;
         n = n+1;
       }
    }

What am I missing ?

Cheers and thanks,

Sophia Drossopoulou

PS Should i have posted this question somewhere else?

 

Coordinator
May 12, 2010 at 10:39 PM

Hi Sophia,

This is indeed the right place to ask these kinds of questions.  However, I'm not able to reproduce what you're describing.  For me, both methods verify successfully.

Are you running from within Visual Studio or from the command line?  Where did you get your Spec# and Boogie from?  Did you build them yourself from the latest sources?  Did you get the binaries from specsharp.codeplex.com and boogie.codeplex.com?  Do you have a recent version of Z3?

I'm guessing the most likely problem is that you have Z3 version 1.?, not version 2.?.  You can get the latest version from http://research.microsoft.com/projects/z3.  Note, until a few weeks ago, Boogie only found version 2.5 or older of Z3 (unless you happened to have copied z3.exe into the Boogie directory yourself).  As of today, it also looks for 2.6, but not yet version 2.7, which is the latest version.  (We need a better solution to this, clearly.)

Another thing you can try in debugging this problem is to add the /arithDistributionAxioms to the SscBoogie command line.  That gives SscBoogie more power in dealing with non-linear arithmetic, even if the underlying prover only supports linear arithmetic.  However, using this switch is in general expensive, so the much better solution is to rely on the prover's support for non-linear arithmetic.

  Rustan

May 13, 2010 at 11:40 AM
Edited May 13, 2010 at 11:42 AM

Hi Rustan,
 
Thank you for the very speedy reply -- indeed a hacker by night!
 
It seems to me that I will have to build everything myself ... gasp.
 
Anyway, just to let you know what happened. I am running SpecSharp from within the IDE. I got Spec# and Boogie from codeplex. I had VisualStudion already, and installed Spec# yesterday, but did not pay too much attention what exctly needed installing, so it may be that I had an old version of z3. After reading your email,  I checked today, and saw that I am running
     Visual Studio 2008  Version 9.0.30729.1 SP
     .NET framework   Version 3.5 SP1
     Microsoft® Spec# Compiler, Version 1.0.21125.0

And as you said: I was running an old version of Z3. Namely, from the Loaded Modules in Software Environment in System Information in About in Help, I obtain 
       z3  1.2.0.0 1.46 MB  17/11/2008 10:54  c:\program files\microsoft\spec#\bin\z3.exe 
       BoogiePlugin 1.0.21125.0 48.00 KB  25/11/2008 14:27  c:\program files\microsoft\spec#\bin\boogieplugin.dll 

Reading your email, I decided to get a new version of Z3. So, I istalled Z3 from codeplex, and then I copied by hand the z3 application into the directory c:\program files\microsoft\spec#\bin.  Indeed, when I checked, I saw that Spec# was using
      z3           2.4.0.0  2.67 MB 17/11/2008 10:54          Microsoft            c:\programfiles\microsoft\spec#\bin\z3.exe

However, when I then ran Spec#, not only did it not find an error in the functions I had written earlier, it did not find errors even in functions which are patently erroneous, eg in 

     void testError(int[] a) 
     ensures a[1]==5;
     {
        a[3]=16;
    }

So, probably I need to just compile the sources.

Cheers,

Sophia