suggestion: translate axioms and implication premises in forward order to coq
ID0002291: This issue was created automatically from Mantis Issue 2291. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002291 | Frama-C | Plug-in > wp | public | 2017-03-13 | 2017-03-13 |
| Reporter | Jochen | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | Silicon-20161101 | OS | xubuntu | OS Version | - |
| Product Version | Frama-C 14-Silicon | Target Version | - | Fixed in Version | - |
Description :
Running "frama-c -wp -wp-prover coq -wp-out wp-out coqtest.c" on the attached file generates two Coq files, viz. "A_eqAxioms.v" and "lemma_goal_Coq.v".
The former contains the translation of "axiomatic eqAxioms", with the axioms ("eqRefl" and "eqTrns") appearing in the same order as in the source. The file "lemma_goal_Coq.v" contains the translation of "axiomatic incAxioms", however, with the axioms ("incLf" and "incRg") appearing in reverse order, compared to the source.
A similar issue concerns the translation of the body formula of axiom "eqTrns", where the first and second premise, viz. "eq(x,y)" and "eq(y,z)" in the source, appear in reverse order in the Coq translation.
(As a side remark: names of locally bound variables could be translated such that a target name closely resembles its source name; for example the source name could appear as a prefix of the target name.)
While probably easy to implement, these suggestions would considerably lower the overall complexity of the user's task.