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

 800help10 Jun 16, 2011 at 8:52 PM Edited Jun 17, 2011 at 2: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);  } } MarkHillebrand Coordinator Jun 18, 2011 at 2: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 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 800help10 Jun 20, 2011 at 3: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? MarkHillebrand Coordinator Jun 20, 2011 at 4: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 800help10 Jun 20, 2011 at 5: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. MarkHillebrand Coordinator Jun 20, 2011 at 6: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 800help10 Jun 21, 2011 at 1:22 PM Edited Jun 21, 2011 at 1: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); } } MarkHillebrand Coordinator Jun 21, 2011 at 8: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