--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on October 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Average Problem




To make this example more visible, I've just add it to Toccata's gallery:

http://toccata.lri.fr/gallery/sum_array.en.html

you will see there which prover I used to prove the VCs. You may also 
have a look at the Coq proofs of the two lemmas if you want.

Last but not least, while doing that I realized that my own 
axiomatization was not quite adequate either, so please look at the web 
page above for a better one.

Notice that this gallery contains some more examples proved using 
Frama-C/Jessie at

http://toccata.lri.fr/gallery/jessieplugin.en.html

- Claude

Le 03/10/2014 08:52, Claude March? a ?crit :
>
> Hello,
>
> Your axiomatization of Sum is probably inadequate. It should be clear in
> your mind if Sum(a,i,j) includes also a[j] or not. Your axioms do not
> seem to be coherent with that respect.
>
> I attach a very similar example coming from the test suite of Jessie
> (available in subdir tests/c of Why distribution).
>
> The two lemmas sum3 and sum_footprint need some induction reasoning to
> be proved, so in the current state of technology in Frama-C + either
> Jessie or WP plugins, an interactive prover like Coq is needed to prove
> them. But you can safely admit them for the rest of the code.
>
> Hope this helps,
>
> - Claude
>
> Le 02/10/2014 18:26, Sebastian a ?crit :
>> Hi,
>> Thank you very much for your previous reply.
>> I followed your instructions and I tried to implement the axiomatic Sum.
>> I am using "Frama-C Neon-20140301" with Alt-Ergo prover on Ubuntu 14.04.
>> I have tried to test it with a simple example but my axiomatic Sum
>> doesn't work and I am not able to find the error.
>> I have made a "functionTest" function that calls "testSum" function with
>> array elements that satisfy the requirements of "testSum" requires
>> clause, but the prover was not able to prove it.
>> I attached the axiomatic Sum definition, the "testSum" function and the
>> "functionTest" function.
>> Could you please suggest how I can proceed with finding a solution to
>> this problem?
>>
>> Thank you very much.
>> Best regards,
>> Sebastian
>>
>>
>>
>> Il 29/09/14 14:12, Lo?c Correnson ha scritto:
>>> Hi,
>>> \sum and \lambda are unsupported with WP.
>>> Instead, you can axiomatize your sum or use an inductive predicate.
>>>
>>> See
>>> http://www.fokus.fraunhofer.de/de/sqc/_download_sqc/ACSL-by-Example.pdf
>>> ? 3.8.1 is a good hint.
>>>     L.
>>>
>>>
>>>
>>> Le 29 sept. 2014 ? 10:00, Sebastian <sdavrieux at gmail.com> a ?crit :
>>>
>>>> Good morning,
>>>>     I'm trying to do the average without overflow, however I'm not
>>>> able to check an assert that contains \sum annotation.
>>>> So I decided to make a simpler function that only uses \sum, but it
>>>> doesn't work. What can I do to solve the problem?
>>>>
>>>> Best regards,
>>>> Sebastian
>>>> <testSum.c>_______________________________________________
>>>> Frama-c-discuss mailing list
>>>> Frama-c-discuss at lists.gforge.inria.fr
>>>> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>>> _______________________________________________
>>> Frama-c-discuss mailing list
>>> Frama-c-discuss at lists.gforge.inria.fr
>>> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>>
>>
>>
>> _______________________________________________
>> Frama-c-discuss mailing list
>> Frama-c-discuss at lists.gforge.inria.fr
>> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>>
>
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           |
Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |