This project is read-only.

verified all base cases in a recursion function, but failed the recursion call

Jun 16, 2011 at 9:52 PM
Edited Jun 17, 2011 at 3:54 AM


 I want to verify a simple recursive palindrome checker but vcc fails at the recursion call. Any suggestions please? And if VCC could verify all the base cases, why the recursion call fails?

 

int palin(int *ar, unsigned len)
 _(requires \thread_local_array(ar,len))
 _(ensures \result == 1 ==> \forall unsigned i;{\match_long(i)} i < len/2 ==> ar[i] == ar[len-1-i])
 _(ensures \result == 0 ==> \exists unsigned i;{\match_long(i)} i < len/2 && ar[i] != ar[len-1-i])
{
 //base case: len == 0 || 1
 if (len <= 1) return 1;
 _(assert 2 <= len)
 if (ar[len-1] != ar[0]) { 
  _(assert \match_long(0))
  _(assert \exists unsigned i;{\match_long(i)} ar[i] != ar[len-1-i])
  return 0;
 } else {
  return palin(ar+1,len-2);
 }
}

 

 

 

 

 

Jun 18, 2011 at 3:53 PM

Hi,

  after the recursive call, VCC needs a little extra help to understand how the elements of the array used in the call ((a+1)[0], (a+1)[1], ..., (a+1)[len - 3]) are related to the original array. The following version works:

#include <vcc.h>

int palin_rec(int *ar, unsigned len)
  _(requires \thread_local_array(ar,len))
  _(returns \forall unsigned i; i < len / 2 ==> ar[i] == ar[len - 1 - i])
{
  int result;

  if (len <= 1) return 1;

  if (ar[len-1] != ar[0]) {
    return 0;
  } else {

    result = palin_rec(ar + 1, len - 2);

    _(assert \forall unsigned i; 0 < i && i < len - 1 ==> ar[i] == (ar + 1)[i - 1])

    return result;
  }
}

Cheers, Mark

Jun 20, 2011 at 4:48 PM

Hi,

Thanks for the help. I tried your version but it still fails.

c:\Temp\vcc\fun contract.c(227,5) : error VC9501: Post condition 'res == expr' did not verify.
c:\Temp\vcc\fun contract.c(220,19) : error VC9599: (related information) Location of post condition.
C:\Program Files\Microsoft Research\Vcc\Headers\vccp.h(222,27) : error VC9599: (related information) from expansion of '_(returns \forall unsigned i; i < len /2 ==> ar[i] == ar[len - 1 - i])'.
Exiting with 3 (1 error(s).)

what version of vcc are you using?

Jun 20, 2011 at 5:36 PM

Hi,

  I am using the June 10 version:

C:\Temp>vcc /version
Microsoft Research Vcc Version 2.1.40610.0
Microsoft Research Boogie Version 2.1.30608.1
Microsoft Research Z3 Version 2.0.41203.1

C:\Temp>vcc /2 s.c
Verification of palin_rec succeeded.

C:\Temp>

  Maybe different options?

Best regards, Mark

Jun 20, 2011 at 6:45 PM

I see, I was using vcc /3

Do you know what's the difference between /2 and /3? And how to bring it to work with /3? Thanks.

Jun 20, 2011 at 7:16 PM

With /3, VCC uses a newer, more high-level memory model. This is shortly mentioned here: http://vcc.codeplex.com/wikipage?title=VCC3&referringTitle=Home.

I don't know why the example breaks, not having used /3 too much myself yet. Maybe Michal can comment...

Best regards, Mark

Jun 21, 2011 at 2:22 PM
Edited Jun 21, 2011 at 2:27 PM

Hi Mark,

It's always hard for me to figure out where extra guidence is needed for VCC to pass the verification. Do you have any suggestions?

For example, for checking if two arrays are equal, VCC verifys eq2, but fails eq1. Sorry for the format, somehow I couldn't paste the code in correct format.

Thanks.

 

 

 

 

int eq1(int *ar1, unsigned len1, int *ar2, unsigned len2) 

_(requires \thread_local_array(ar1,len1))

_(requires \thread_local_array(ar2,len2))

_(returns (len1 == len2) && (\forall unsigned i; i < len1 ==> ar1[i] == ar2[i]))

{

if (len1 != len2) {

return 0;

}

 

if (len1 <= 0) return 1; //otherwise can't prove ar1[len1-1] is readable

if (ar1[0] != ar2[0]) {

 

return 0;

} else {

int t = ex2(ar1+1,len1-1,ar2+1,len2-1);

_(assert \forall unsigned i; 0 < i && i < len1-1 ==> ar1[i] == (ar1+1)[i-1])

_(assert \forall unsigned i; 0 < i && i < len2-1 ==> ar2[i] == (ar2+1)[i-1])

return t;

}

}

 

 

//check for equal arrays

int eq2(int *ar1, unsigned len1, int *ar2, unsigned len2)

_(requires \thread_local_array(ar1,len1))

_(requires \thread_local_array(ar2,len2))

_(returns (len1 == len2) && (\forall unsigned i; i < len1 ==> ar1[i] == ar2[i]))

{

if (len1 != len2) {

return 0;

}

 if (len1 <= 0) return 1; //otherwise can't prove ar1[len1-1] is readable

if (ar1[len1-1] != ar2[len2-1]) {

return 0;

} else {

return ex2(ar1,len1-1,ar2,len2-1);

}

}

Jun 21, 2011 at 9:07 PM

Hi there,

  your example works with the following assertions, which include also the last element:

_(assert \forall unsigned i; 0 < i && i < len1 ==> ar1[i] == (ar1+1)[i-1])
_(assert \forall unsigned i; 0 < i && i < len2 ==> ar2[i] == (ar2+1)[i-1])

  Cheers, Mark