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] Combining Simplify and Coq

Hello,

Le lun. 07 juin 2010 22:50:10 CEST,
Pascal Cuoq <pascal.cuoq at gmail.com> a ?crit :

> > Now for the remaining VCs I planned to prove with Coq, I know I can use:
> > frama-c -jessie-analysis -jessie-atp coq file.c
> > This creates a file file.jessie/coq/file_why.v, which I can open with the
> > coqide, and start filling in the proves.
> >
> "Filled in" would require automatic provers to generate checkable
> proof certificates,
> which they don't with a few exceptions. Indeed sometimes automatic provers
> have correctness bugs and validate VCs that are later found to be false.
> "Assumed" is the best you can expect.
> 

Pascal is right: except for zenon, which does not have built-in support
for arithmetic, and is thus more or less unsuitable on the proof
obligations generated by jessie/why, almost no prover is able to
generate a Coq proof, although alt-ergo is moving toward this
direction. 
However, if you're ready to trust the automated provers (and you're
implicitely doing that each time you don't use -jessie-atp coq ;-), it
is possible to call them from the coq proof assistant itself, via a
binding to Why, thanks to the work of Nicolas Ayache. 
Unfortunately, this feature has not been really maintained, and for the
current stable version 8.2pl1, this is only available via a patch
present in the godi (http://godi.camlcity.org/) distribution of Coq.
I've understood that this feature has been re-implemented in the
unstable version 8.3beta, but I never used it.

The extension allows you to use the "tactics" ergo, simplify and z3,
that will call the corresponding prover, so if you have an appropriate
version of coq, frama-c -jessie-analysis -jessie-atp coq
-jessie-why-opt="-coq-tactic ergo" file.c will only ask you to provide
a coq script for the proof obligations that alt-ergo is not able to
discharge[1]

-- 
E tutto per oggi, a la prossima volta.
Virgile
[1] You might want to use a slightly longer timeout, as for some reason
launching the prover from coq rather than from Gwhy seems somewhat
longer - my best guess would be that the encoding of formulas is
slightly more complicated. This is done by 'Dp_timeout n.' in the coq
file (where n is the number of seconds you are ready to wait for each
proof obligation).