Code template for a invariant contract clause. Eiffel Software invariant code