--- layout: fc_discuss_archives title: Message 51 from Frama-C-discuss on May 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] question about a simple example and jessie



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.
>