For now, we could simply deactivate these invariants. For the test cases there are not needed. But as a showcase for automatically generating JML they are quite sufficient.
But you also want to use these invariants outside of the scope of this record.
I would still prefer class axioms, which should become Taclets.
Also better, the introduction of named (static) invariants, which are then not automatically added, and the extension of \static_invariant_for(obj, name) to put them on the sequent.
My final suggestion would be:
//@ public explicit static invariant_free taut1: 1+1==2;
The explicit modifier (present in C++) marks that the invariant is not implicitly added to $inv (only possible with free inv), and need to grasp explicitly.
I would also say, we should a warning or synonym on axiom (and treat thi as an invariant_free).
Originally posted by @wadoon in #3758 (comment)
For now, we could simply deactivate these invariants. For the test cases there are not needed. But as a showcase for automatically generating JML they are quite sufficient.
But you also want to use these invariants outside of the scope of this record.
I would still prefer class axioms, which should become Taclets.
Also better, the introduction of named (static) invariants, which are then not automatically added, and the extension of
\static_invariant_for(obj, name)to put them on the sequent.My final suggestion would be:
The explicit modifier (present in C++) marks that the invariant is not implicitly added to
$inv(only possible with free inv), and need to grasp explicitly.I would also say, we should a warning or synonym on
axiom(and treat thi as aninvariant_free).Originally posted by @wadoon in #3758 (comment)