Code template contract to ensure a class attribute remains unchanged during the execution of a routine Eiffel Software unchanged Eiffel code contract postcondition