Trouvez l'invariant de boucle pour cet algorithme qui calcule le maximum d'un tableau.

int maximum(int t[], int n) {
    if (n == 0) return -1;
    int max = t[0], k = 1;
    while (k < n) {
        if (t[k] > max) max = t[k];
        k++;
    }
    return max;
}

Invariant de boucle :

Valider