Code template contract predicate to ensure an attached test contract Eiffel Software attached Eiffel code contract invariant precondition postcondition