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