Loop invariante de búsqueda lineal

Como se ve en Introducción a los algoritmos http: //mitpress.mit.edu/algorithm), el ejercicio establece lo siguiente:

Input: Array A [1 ... n]

Salida: i, donde A [i] = v o NIL cuando no se encuentra

Escriba un pseudocódigo para la BÚSQUEDA LINEAL, que explora la secuencia, buscando v. Usando un bucle invariante, pruebe que su algoritmo es correcto. (Asegúrese de que su bucle invariante cumpla con las tres propiedades necesarias: inicialización, mantenimiento, terminación).

No tengo problemas para crear el algoritmo, pero lo que no entiendo es cómo puedo decidir cuál es mi invariante de bucle. Creo que entendí el concepto de invariante de bucle, es decir, una condición que siempre es verdadera antes del comienzo del bucle, al final / comienzo de cada iteración y sigue siendo cierta cuando finaliza el bucle. Este suele ser el objetivo, por ejemplo, en el orden de inserción, iterando sobre j, comenzando en j = 2, los elementos [1, j-1] siempre se ordenan. Esto tiene sentido para mí. Pero para una búsqueda lineal? No puedo pensar en nada, simplemente suena demasiado simple para pensar en un bucle invariante. ¿Entendí algo mal? Solo puedo pensar en algo obvio como (es NIL o entre 0 y n). ¡Muchas gracias por adelantado

Respuestas a la pregunta(7)

Su respuesta a la pregunta