--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on July 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Prove the reverse of a char*, ensure problems



Hi at all!

I'm trying to prove this recursive function (I want to prove THE recursive version of this function):

void reverse(char *s, unsigned n)
{
    if (n < 2)
        return;
     
    swap(s, s + (n - 1));
    reverse(s + 1, n - 2);
}    

(Swap is already proved)

It's days that I try do get it to be proved, but I can't. What am I doing wrong?

Here is the FramaC code:

/*@
    requires n >= 0;
    requires \valid(s+(0 .. n-1));
 
    assigns s[0..(n-1)];
 
    ensures reversed_recursive{Pre,Post}(\at(s, Pre), \at(s, Post), n);
     
    ensures \forall unsigned i;
        0 <= i < n ==> \at(s[i], Pre) == \at(s[n-i-1], Post);

    ensures \at(s, Pre) == get_reverse{Post}(\at(s, Post), n);
 
*/

As you can see, I put three ensures. It's because I want at least one to be proved...

/*@
    logic char* get_reverse{L}(char *s, integer n) =
        n < 2 ?
            s :
            get_reverse(s+1, n-2);
*/

/*@
    predicate reversed_recursive{L1,L2}(char *a, char *b, integer n) =
        n <= 1 ?
        \at(*a, L1) == \at(*b, L2) :
        (\at(a[0], L1) == \at(b[n-1], L2)) && reversed_recursive{L1,L2}(\at(a+1, L1), \at(b, L2), n-1);
*/
 
/*@
    predicate reversed_iterative{L1,L2}(char* a, char* b, unsigned n) =
        \forall unsigned i;
        0 <= i < n ==> \at(a[i], L1) == \at(b[n-i-1], L2);
*/

What am I doing/thinking wrong?


Thanks,
Francesco. 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150720/7a326b60/attachment.html>