Invariants

NYI: Invariants are not supported yet.

The basic idea is that an invariant must hold after the execution of its feature, just like a postcondition. Additionally, the invariant must hold whenever an inner feature is called or returns from a call, so it is part of all pre- and post-conditions of its inner features.