--- layout: fc_discuss_archives title: Message 51 from Frama-C-discuss on May 2010 ---
Naghmeh Ghafari wrote: > I was trying to verifying the same code using Frama-C. Even if I > translate the second loop_assert for the inner loop as following: > > @ loop invariant \forall int a,b; ((aux < a <= i+1) && (aux < b <= > i+1) ==> (a <= b ==> arr[a] <= arr[b])); > Indeed, I cannot confirm that this is equivalent to the HAVOC invariant _be_cause __it_is very _hard to __read __havoc_syntax :-) You could simplify your formula into @ loop invariant \forall integer a,b; aux < a <= b <= i+1 ==> arr[a] <= arr[b]; and I believe it is almost the correct invariant to use for proving your bubble sort. I suggest now to forgot about HAVOC invariant and start thinking to see if it is really the proper invariant: is it aux < a or aux <= a ? is it i+1 or i ? Take a paper and write that down, you should find to correct formula. - Claude > (which I am not sure if it is completely equivalent to the HAVOC > notation), I still cannot use Frama-C to verify this code. Then I > tried the implementation that was suggested by Pascal (on this mailing > list) and I cannot verify even th eother implementation using > Frama-C. I am relatively new to both tools. I have worked with Boogie > and Z3 before, but not with HAVOC front end, so now exploring both > HAVOC and jessie plugin at the same time. That's why I am trying to > use the same implementation. I really appreciate any help and > suggestions. >