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

[Frama-c-discuss] Average Problem



Thank you very much! It works perfectly!
Now I'm able to solve Average Problem and it seems to work.

Best regards,
Sebastian

Il 03/10/14 09:51, Claude March? ha scritto:
>
>
> 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
>>
>