--- layout: fc_discuss_archives title: Message 10 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



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,
-- 
E tutto per oggi, a la prossima volta
Virgile