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

[Frama-c-discuss] Axiomatic Definition of Rounding Function (Claude March?)



Thanks for the experiment with different provers. I have reformulated
the assertions as lemmas as suggested and run the Coq prover on the
example, but also this one is not able to prove the lemmas.

As for the second axiom: I have learned that if one defines a function
one has to ensure that the function value exists (for total functions)
and that it is unique. It was not there in my first attempts but I
have seen it somewhere so I thought I may help the prover.

Frank