--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on November 2014 ---
Hi Sebastian, Proving your assertions from the axioms you gave requires an induction. Automated provers cannot do that. Here is a better definition. The four lemmas are proved by Z3 /*@ axiomatic Floor { @ logic integer floor(real a); @ axiom floor: \forall real a; floor(a) <= a <= floor(a)+1; @ } @*/ //@ lemma floor01: floor(0.1) == 0; //@ lemma floor105: floor(10.5) == 10; //@ lemma floorm01: floor(-0.1) == -1; //@ lemma floorm105: floor(-10.5) == -11; - Claude Le 18/11/2014 10:00, Sebastian a ?crit : > Hi, > I tried to use \floor but it raised an error: > "The full backtrace is: > Raised at file "hashtbl.ml", line 353, characters 18-27 > Called from file "hashtbl.ml", line 361, characters 22-38 > Plug-in wp aborted: internal error. > Reverting to previous state. > Look at the console for additional information (if any). > Please report as 'crash' at http://bts.frama-c.com/. > Your Frama-C version is Neon-20140301. > Note that a version and a backtrace alone often do not contain enough > information to understand the bug. Guidelines for reporting bugs are at: > http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines" > > > So I tried to implement an axiomatic floor function. > 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 floor > doesn't work and I am not able to find the error. > I have made a "testFloor" function with > assert clauses, but the prover was not able to prove it. > I attached the axiomatic Floor definition and the "testFloor" function. > Could anyone please suggest how I can proceed with finding a solution to > this problem? > > Thank you very much, > Sebastian > > > _______________________________________________ > 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 -------------- section suivante -------------- Une pi?ce jointe HTML a ?t? nettoy?e... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141118/ad949ee5/attachment.html>