--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on July 2015 ---
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>