Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Prove the reverse of a char*, ensure problems
  • From: fbonizzi at hotmail.it (Francesco Bonizzi)
  • Date: Mon, 20 Jul 2015 22:56:03 +0200
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>