--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on February 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] names of clauses, invariants, axioms



And just to be clear - you mean a predicate with zero arguments as in 
P(), not as P.

- David

On 2/16/2016 9:58 AM, Virgile Prevosto wrote:
> Hello David,
>
> 2016-02-16 13:40 GMT+01:00 cok at frontiernet.net <cok at frontiernet.net>:
>> Terms and predicates in ACSL can be given labels. In addition, some clauses,
>> such as invariants and axioms require an identifier. The ACSL 1.10 document,
>> at least, states that expression labels are purely for readability (and
>> perhaps error messages) and may not be used in other expressions (p. 17).
>>
>> Is the same true (in ACSL) for identifiers of invariants and axioms?
>> (Frama-C (Sodium) does not support invariants, and does not allow the
>> identifier of an axiom to be used as a predicate symbol).
>>
>> If not, this would be a useful feature - particularly for weak invariants.
> Axioms' names do not play any role in the current implementation. On
> the other hand, an invariant is also a predicate, with either 0 (for
> global invariants) or 1 (for type invariants) argument, and can be
> used as such. As you said, this is mainly useful for weak invariants,
> to assert that they hold at an arbitrary point beyond a function pre-
> or post-state.
>
> Best regards,