Suggest to close a section if each obligation is proven by *some* prover
ID0000602: This issue was created automatically from Mantis Issue 602. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000602 | Frama-C | Graphical User Interface | public | 2010-10-12 | 2010-10-13 |
| Reporter | Jochen | Assigned To | monate | Resolution | not fixable |
| Priority | normal | Severity | feature | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Boron-20100401 | Target Version | - | Fixed in Version | - |
Description :
Currently, a section (like e.g. "fctxxx default behaviour" is automatically closed when one prover was able to prove all its contained obligations. However, often no single prover can prove them all, but each of them can be proved by some prover (i.e. in each line a green bullet appears, although not in the same column).
As a result, the user has to check all lines by himself, which is tedious (and even error-prone) when sections are large and the process of finding an adequate and verifiable specification involves many edit->vcg->prove cycles.
Therefor, I suggest to close a section once the statistics count has reached 100% of proven obligations (i.e. n/n). A "summary column" could be introduced showing a green bullet for single a obligation if it was proven by some prover, and a green check-mark for a section if its statistics count is 100%. For "very large" programs, it might even be desirable to have an icon summarizing all sections, i.e. the whole program, in a corresponding way.