Verificació de max_min2 Z40094

Considera la següent funció:

/* @pre  v.size()>0
*  @post el primer component del resultat és el valor màxim de v,
*        el segon component del resultat és el valor mínim 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;
}

Ara respon a les següents preguntes:

Pregunta 1
Escriu l’invariant del bucle del codi max_min2.

Pregunta 2
Demostra que si es compleix la precondició, després d’executar les inicialitzacions, es compleix l’invariant.

Pregunta 3
Demostra que si es compleixen la condició d’entrada en el bucle i l’invariant, i s’executa el cos del bucle, llavors es torna a complir l’invariant.

Pregunta 4
Demostra que si es compleix l’invariant, però no la condició d’entrada, llavors es compleix la postcondició.

Pregunta 5
Demostra que el bucle acaba. És a dir, dóna’m la funció cota i demostra les seves propietats.

Observació

El fitxer a enviar ha de ser un .tar dins del qual hi hagi un fitxer de text respostes.txt amb les respostes a les preguntes. (El veredicte del Jutge sempre serà verd, perquè les respostes s’avaluaran manualment.)