# 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] question about a simple example and jessie

*Subject*: [Frama-c-discuss] question about a simple example and jessie*From*: Claude.Marche at inria.fr (Claude Marche)*Date*: Sun, 16 May 2010 08:34:36 +0200*In-reply-to*: <4BEC85F3.3000408@cslabs.com>*References*: <4BDF2C15.5010201@cslabs.com> <4BEAC8E6.1050107@inria.fr> <4BEC85F3.3000408@cslabs.com>

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

**References**:**[Frama-c-discuss] question about a simple example and jessie***From:*naghmeh.ghafari at cslabs.com (Naghmeh Ghafari)

**[Frama-c-discuss] question about a simple example and jessie***From:*Claude.Marche at inria.fr (Claude Marche)

**[Frama-c-discuss] question about a simple example and jessie***From:*naghmeh.ghafari at cslabs.com (Naghmeh Ghafari)

- Prev by Date:
**[Frama-c-discuss] question about a simple example and jessie** - Next by Date:
**[Frama-c-discuss] question about a simple example and jessie** - Previous by thread:
**[Frama-c-discuss] question about a simple example and jessie** - Next by thread:
**[Frama-c-discuss] volatile type qualifiers** - Index(es):