explain wp's syntactic restrictions on "inductive" definitions
ID0002337: This issue was created automatically from Mantis Issue 2337. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002337 | Frama-C | Documentation | public | 2017-12-14 | 2019-10-17 |
| Reporter | Jochen | Assigned To | correnson | Resolution | no change required |
| Priority | normal | Severity | text | Reproducibility | N/A |
| Platform | Sulfur-20171101 | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
In Sect.2.6.3 "Inductive predicates" (p.50) of the manual "acsl-implementation-Sulfur-20171101.pdf", it is announced that "tools might enforce syntactic conditions on the form of inductive definitions". However, in the Wp manual (file "wp-manual-Sulfur-20171101.pdf") the string "inductive" doesn't occur at all. It should be explained there what restrictions Wp enforces on "inductive" definitions; in case it doesn't restrict them at all, this should be mentioned, too. I didn't check other plugin manuals for the occurrence of the string "inductive".
As a side remark: From a user's point of view, the freedom of each plugin to give its own semantics to (details of) ACSL constructs is confusing, and sometimes even annoying. From a software engineer's point of view, admitting too much freedom to plugins gives away the advantages of a integerated framework/plugin architecture. Having different semantics for ACSL details may compromise the interoperability of plugins.