Additive semantics for multiple contracts

acsl-language / acsl

Sources for the ANSI/ISO C Specification Language manual

Other

49 stars 8 forks source link

Additive semantics for multiple contracts #8

Open vprevosto opened 7 years ago

vprevosto commented 7 years ago

In case of multiple contracts, all clauses are merged. This semantics is arguably dangerous, e.g. if one does only include a part of the contracts of a called function when performing modular verification, some requires clauses might not be checked.

Should this behavior be forbidden?
Should we distinguish between an initial contract and complementary one (such as the also mechanism of JML)?

davidcok commented 6 years ago

The issue in JML is complicated by inheritance (and will be in ACSL++ as well). In ACSL it is complicated by contracts appearing in .h files and thus perhaps being included more than once. One thought is that behaviors in contracts with the same behavior id might be required to be syntactiically identical (identical token streams, not necessarily white space). A required 'also' at least alerts a careful reader that there are other behaviors to be considered.