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

[Frama-c-discuss] Average Problem



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
>

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

-------------- section suivante --------------
Une pi?ce jointe autre que texte a ?t? nettoy?e...
Nom: sum_array.c
Type: text/x-csrc
Taille: 3796 octets
Desc: non disponible
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141003/4c89ea7a/attachment.c>