Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Axiomatic Definition of Rounding Function (Claude March?)
  • From: frank at dordowsky.de (Frank Dordowsky)
  • Date: Tue, 24 Jun 2014 21:03:00 +0200 (CEST)
  • In-reply-to: <mailman.21.1403517683.1944.frama-c-discuss@lists.gforge.inria.fr>
  • References: <mailman.21.1403517683.1944.frama-c-discuss@lists.gforge.inria.fr>
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