Verificación de max_min2 Z40094

Considera la siguiente función:

/* @pre  v.size()>0
*  @post el primer componente del resultado es el valor maximo de v,
*        el segundo componente del resultado es el valor minimo de v
*/
pair<int, int> max_min2(const vector<int>& v) {
    pair<int, int> p;
    p.first = v[0];
    p.second = v[0];
    int i = 1;
    while (i < v.size()) {
        if (v[i] > p.first) {
            p.first = v[i];
        } else if (v[i] < p.second) {
            p.second = v[i];
        }
        ++i;
    }
    return p;
}

Ahora responde a las siguientes preguntas

Pregunta 1
Escribe el invariante del bucle del código max_min2.

Pregunta 2
Demuestra que si se cumple la precondición, después de ejecutar las inicializaciones, se cumple el invariante.

Pregunta 3
Demuestra que si se cumplen la condición de entrada en el bucle y el invariante, y se ejecuta el cuerpo del bucle, entonces se vuelve a cumplir el invariante.

Pregunta 4
Demuestra que si se cumple el invariante, pero no la condición de entrada, entonces se cumple la postcondición.

Pregunta 5
Demuestra que el bucle acaba. Es decir, dame la función cota y demuestra sus propiedades.

Observación

El fichero a enviar debe ser un .tar dentro del cual haya un fichero de texto respuestas.txt con las respuestas a las preguntas. (El veredicto del Jutge siempre será verde, porque las respuestas se evaluarán manualmente.)