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

[Frama-c-discuss] Floor problem



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>