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