Frama-C Bug Tracking System - Frama-C
View Issue Details
0002337Frama-CDocumentationpublic2017-12-14 13:432019-10-17 17:19
closedno change required 
0002337: explain wp's syntactic restrictions on "inductive" definitions
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.
No tags attached.
Issue History
2017-12-14 13:43JochenNew Issue
2017-12-29 11:57signolesAssigned To => correnson
2017-12-29 11:57signolesStatusnew => assigned
2017-12-29 12:02signolesNote Added: 0006500
2019-10-17 17:14corrensonStatusassigned => resolved
2019-10-17 17:14corrensonResolutionopen => no change required
2019-10-17 17:19signolesStatusresolved => closed

2017-12-29 12:02   
The semantics of ACSL is (or should be) the same for all plug-ins. About inductive definitions, the ACSL manual only warns the user that plug-ins might add __syntactic__ restrictions because most of them cannot handle the most general form of ACSL inductive definition.