Wanted features related to Why3-Coq
This is a follow up on frama-c/frama-c#956 and discussion we had with Jens on the ACSL by Example GitLab about Coq via Why3 in Frama-C.
At least two features could be added to make it easier to use (in particular for ACSL by Example):
- drivers that are only applied to Coq (or any prover), an that can be verified,
- user defined (restricted) context for the proof of lemmas in Coq.
This shall be the job of the driver. We probably need to a way to refine the why3 context per prover. Then, it is easy to enrich the Task generated by
ProverWhy3, which is already « prepared » in a specific way for each prover.
Currently, the supported import directives for WP drivers are:
why3.file="mydir/foo.why" why3.file="mydir/foo.why:Bar" why3.file="mydir/foo.why:Bar:T" why3.import="foo.Bar" why3.import="foo.Bar:T"
@lcorrenson suggests to reformulate all of them into something fully understandable from why3 users:
[for "myProver",...] loadpath "path/to/dir"; [for "myProver",...] import foo.Bar [as T];
This is indeed more flexible than using our custom
If we have two files like:
lemma Foo: // ... lemma To_Prove: // uses Foo
lemma Bar: // ... lemma Foo: // ... lemma To_Prove: // uses Foo
The two files generate different proof contexts for lemmas, because even if
To_Prove only needs
Foo, WP collects all lemmas that appear before
To_Prove. This is why I suggest to provide the user with a way to specify precisely the proof context so that it can remain the same from a file to another.
I think we could create an ACSL extension like:
/*@ lemma Foo: ... lemma Bar: ... lemma Proved_with_Coq: ... lemma_dependencies Proved_with_Coq: Foo ; */
So that the user can restrict the proof context of the lemma can be as simple and predictable as possible. Note that we should check that it compatible with the