| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0002100 | Frama-C | Plug-in > wp | public | 2015-03-31 17:15 | 2019-10-17 18:03 | ||||
| Reporter | jens | ||||||||
| Assigned To | correnson | ||||||||
| Priority | normal | Severity | minor | Reproducibility | always | ||||
| Status | closed | Resolution | won't fix | ||||||
| Product Version | Frama-C Sodium | ||||||||
| Target Version | Fixed in Version | ||||||||
| Summary | 0002100: readability of coq(?) names | ||||||||
| Description | Consider the following ACSL lemma: /*@ lemma X : \forall integer a, b; (a+b)*(a-b) == a*a - b*b; */ which is automatically discharged by alt-ergo. When I open the proof obligation in Coq, the lemma looks like follows: Goal forall (i_1 i : Z), (((i_1 * i_1) = ((i * i) + ((i + i_1) * (i_1 - i))))%Z)%Z. Under Neon the proof coq representation preserves the original names much better Goal forall (a_0 b_0 : Z), (((a_0 * a_0) = ((b_0 * b_0) + ((a_0 + b_0) * (a_0 - b_0))))%Z)%Z. The problem gets worse with more parameters. | ||||||||
| Steps To Reproduce | frama-c-gui -wp lemma.c | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
||||||
|
||||||
 Relationships |
| Notes |
|
|
jens (reporter) 2015-03-31 17:21 |
I wonder whether this is related to my previous request for "better" coq names... https://bts.frama-c.com/view.php?id=1630 |
|
jens (reporter) 2015-04-10 10:39 |
The "obfuscated" names generated by WP make it quite hard to work on coq proofs for functions with several arguments. Would it be possible to return to the naming scheme of Neon? |
|
correnson (manager) 2015-04-10 11:16 |
No it is not that easy. We need to find a solution to keep user names while still preserving our new very efficient locally-nameless implementation of binders in Qed... |
|
correnson (manager) 2015-06-29 17:16 |
We plan de completely rewrite the Coq output of goals to make them more readable. |
|
Jochen (reporter) 2017-10-09 17:19 |
I suspect that the (different) renaming (in lemmas and goals) even may lead to a worse verification rate, cf. issue 0002329 for details. |
|
correnson (manager) 2019-10-17 17:36 |
Coq output is now deprecated and will be abandoned in future releases. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2015-03-31 17:15 | jens | New Issue | |
| 2015-03-31 17:15 | jens | Status | new => assigned |
| 2015-03-31 17:15 | jens | Assigned To | => correnson |
| 2015-03-31 17:15 | jens | File Added: lemma.c | |
| 2015-03-31 17:21 | jens | Note Added: 0005837 | |
| 2015-04-10 10:39 | jens | Note Added: 0005877 | |
| 2015-04-10 11:16 | correnson | Note Added: 0005879 | |
| 2015-06-29 17:16 | correnson | Note Added: 0005961 | |
| 2015-06-29 17:16 | correnson | Status | assigned => acknowledged |
| 2015-09-01 12:03 | correnson | Relationship added | related to 0002153 |
| 2017-10-09 17:19 | Jochen | Note Added: 0006465 | |
| 2019-10-17 17:36 | correnson | Note Added: 0006913 | |
| 2019-10-17 17:36 | correnson | Status | acknowledged => resolved |
| 2019-10-17 17:36 | correnson | Resolution | open => won't fix |
| 2019-10-17 18:03 | signoles | Status | resolved => closed |
| Issue History |