explain wp's syntactic restrictions on "inductive" definitions
ID0002337: This issue was created automatically from Mantis Issue 2337. Further discussion may take place here.
|Reporter||Jochen||Assigned To||correnson||Resolution||no change required|
|Product Version||-||Target Version||-||Fixed in Version||-|
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.