--- layout: fc_discuss_archives title: Message 34 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,
There are several issues you face with.
1. Defining the \floor builtin (undefined by default in Neon)
2. Axiomatizing a \floor function such that Alt-Ergo can reason about it
The tow points are discussed in turn below.

Point 1. is easily handled by using wp drivers (Cf. User Manual, option -wp-driver)
Using driver, you can state that a logic predicate is equal to another function already defined in other place.
And you can also ask WP to use supplementary Alt-Ergo, Coq and Why-3 files.
You should have a look to file `<frama-c-share>/wp/wp.driver` for syntax example.
It is interesting to notice that WP translates a double d into an int with `to_uint32(truncate (d))`.
So in your case, you should use a driver directive like:
```
logic real \floor(real) = "truncate" ;
```
However, I?m afraid `truncate` is not yet axiomatized completely, but you can provide supplementary axioms about the `truncate` function on your own.

Point 2. is not easy. Basically, all your axioms can not be instantiated by Alt-Ergo, or are infinitely instantiated and Alt-Ergo is overwhelmed.
In your case, just remark that floor(x) = floor(x-1)+1 can be instantiated infinitely many times? You should document yourself about `triggers`.
When you can not rely on triggers, you can finely control instantiation by using so-called `lemma functions`:

// This is a `standard` lemma:
//@ lemma FloorSmall : \forall real e ; 0.0 <= e < 1.0 ==> \floor(e) == e ;

// This is a `lemma function`:
//@ predicate FloorInt(integer k, real e) = \floor(k+e) = k + \floor(e);
//@ lemma FloorInt_correct : \forall integer k,real e; FloorInt(k,e);


These two lines are equivalent to asserting \forall k,e; \floor(k+e) = k+\floor(e) directly,
But this formulation allows you to perform instantiations by hand wherever you need it:

{
	?
	//@ assert A: FloorInt( 10 , 0.5 );
	//@ assert B: \floor(10.5) == 10.0 ;
}

(A) will be discharged by FloorInt_correct
(A) will be inlined by Alt-Ergo as \floor( 10.0 + 0.5 ) = 10.0 + \floor(0.5)
(B) will be finally discharged by FloorSmall

Remark: you can turn these lemmas into axioms if you want to axiomatize \floor.
Or you can prove them with Coq by using your axioms.

Regards,
L.

Le 18 nov. 2014 ? 10:00, Sebastian <sdavrieux at gmail.com> 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
> <testFloorAssiomatica.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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141118/740e831a/attachment-0001.html>