[Why3-club] Generating Coq with Why3 into separate files

Julien Thierry thierry at adacore.com
Fri Mar 7 14:21:13 CET 2014


Dear Why3-Club,

In the case of generation to manual prover like Coq from a WhyML file, we
would like to separate the part generated by Why3 and the part that should
be edited into different files as is already the case for Isabelle.

One possible model could be having three files:
- one generated containing a proposition corresponding to a Why3 goal (and
axioms)
- one manually editable to prove the proposition (which wont be generated
if already existing)
- one generated to verify that the proof file actually proves the right
predicate

I'm joining file corresponding to a simple example to illustrate the model:
test.v contains the predicate, proof_test.v the proof manually editable and
check_proof_test.v the verification.

The question is, would that be a viable model? Is there a better way to
split the goal and the proof into different files?

Best regards,

-- 
Julien Thierry
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: check_proof_test.v
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20140307/c889fa4f/attachment.ksh>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: test.v
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20140307/c889fa4f/attachment-0001.ksh>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: proof_test.v
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20140307/c889fa4f/attachment-0002.ksh>


More information about the Why3-club mailing list