--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on October 2014 ---
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 |