[TP09] Somme cumulée - Invariant - [LINFO1103] Introduction à l'algorithmique

[TP09] Somme cumulée - Invariant

La fonction suivante renvoie un tableau dont les éléments sont les sommes cumulées des éléments d'un tableau reçu en paramètre.

def cum_sum(t):
    """
    pre: `t` un tableau d'entiers
    post: `t_cum` un tableau d'entiers de taille len(t) dont les éléments sont les sommes cumulées de `t`
    """
    cum_sum_i = 0
    t_cum = [0] * len(t)
    for i in range(len(t)):
        cum_sum_i += t[i]
        t_cum[i] = cum_sum_i
    return t_cum

Vérifiez la correction de la fonction. Pour prouver la correction d'un algorithme itératif, il faut montrer trois choses :

l'invariant est vérifié après l'initialisation de toutes les variables de la boucle, juste avant la première itération
l'invariant est vérifié à chaque itération, après que toutes les instructions de la boucle ont été exécutées
vu la condition d'arrêt de la boucle, la post-condition découle de l'invariant.

Pour cela, vous aurez besoin de réécrire la boucle en utilisant un while.

Copiez-collez cette commande dans votre terminal :

Le mot de pase pour se connecter est

Question 1: Définir l'invariant

Pour trouver l'invariant, nous allons analyser un exemple simple. Supposons qu'on ait en entrée le tableau t suivant :

t = [1, 1, -1, -1, 1]

Juste après l'initialisation, le tableau t_cum ne contient que des 0 et i se trouve à la première position :

t_cum = [0, 0, 0, 0, 0]
i = 0

Si on regarde les états du programme après la dernière instruction de la boucle pour les trois premiers passages dans le while, on observe ceci :

    t_cum          i      cum_sum_i
[1, 0, 0, 0, 0]    1         1
[1, 2, 0, 0, 0]    2         2
[1, 2, 1, 0, 0]    3         1

Qu'observe-t-on à la fin de chaque itération ? Sélectionnez, parmi les propositions suivantes, celle(s) qui est (sont) respectée(s) à la fin de chaque itération.

Chacun des éléments du tableau t contient la somme cumulée attendue

Chacun des i premiers élément du tableau t_cum contient la somme cumulée attendue

La variable cum_sum_i \(\geq 0\)

La variable cum_sum_i contient la somme des i premiers éléments de t

Question 2: Initialisation

L'invariant peut être formalisé comme suit :

\begin{align*} \forall j \in \{0:(i-1)\} \colon \mathit{t\_cum}[j] & = \sum_{k=0}^{j} t[k] \\ \mathit{cum\_sum\_i} & = \sum_{j = 0}^{i-1} t[j] \end{align*}

La notation \(\forall j \in \{0:(i-1)\}\) signifie pour toutes les valeurs j comprises dans l'ensemble des entiers allant de 0 à i-1.

L'invariant est-il vérifié après l'initialisation ? Sélectionnez, parmi les propositions suivantes, celle qui répond à la question précédente.

Remarque sur la notation \(\{k:l\}\)

La notation \(\{k:l\}\) permet d'énoncer une propriété sur les éléments de t_cum et représente l'ensemble des entiers plus grands ou égal à k et plus petit ou égal à l. Si k > l, l'ensemble \(\{k:l\}\) est vide, ainsi que le sous-tableau correspondant. À part dans ce cas-là, les indices k et l doivent être dans les bornes acceptables de t_cum sinon le résultat serait une erreur.

Après l'initialisation, i \(=0\). Étant donné qu'il n'y a aucun entier compris dans l'ensemble \(\{0:-1\}\), les deux parties de l'invariant sont trivialement vérifiées

Après l'initialisation, i \(=1\). Étant donné que l'ensemble \(\{0:0\}\) ne contient qu'un seul élément,

\begin{align*} \mathit{t\_cum}[0] & = \sum_{k=0}^{0} t[k] = t[0] \\ \mathit{cum\_sum\_i} & = \sum_{j = 0}^{0} t[j] = t[0] \end{align*}

Les deux parties de l'invariant sont donc vérifiées.

Question 3: Itération

L'invariant est-il conservé par l'exécution d'une itération ?

Sélectionnez, parmi les propositions suivantes, celle(s) qui est (sont) correcte(s).

Par hypothèse, au début de la boucle, cum_sum_i contient la somme des i premiers éléments de t. Cette valeur est mise à jour en y ajoutant l'élément t[i-1]. La variable cum_sum_i contient donc maintenant \(\sum_{j=0}^{i-1} t[j]\). La dernière instruction de la boucle est d'incrémenter la variable i d'une unité. On retrouve donc exactement l'invariant spécifié plus haut.

Par hypothèse, au début de la boucle, cum_sum_i contient la somme des i premiers éléments de t. Cette valeur est mise à jour en y ajoutant l'élément t[i+1]. La variable cum_sum_i contient donc maintenant \(\sum_{j=0}^{i+1} t[j]\). La dernière instruction de la boucle est d'incrémenter la variable i d'une unité. On retrouve donc exactement l'invariant spécifié plus haut.

Par hypothèse, chacun des i premiers élément du tableau t_cum contient la somme cumulée attendue. Ce tableau est mis à jour en y ajoutant, à l'indice i, la nouvelle valeur de cum_sum_i. La variable t_cum respecte donc la propriété suivante : \(\forall j \in \{0:i\} \colon \mathit{t\_cum}[j] = \sum_{k=0}^{j} t[k]\). La dernière instruction de la boucle est d'incrémenter la variable i d'une unité. On retrouve donc exactement l'invariant spécifié plus haut.

Par hypothèse, au début de la boucle, cum_sum_i contient la somme des i premiers éléments de t. Cette valeur est mise à jour en y ajoutant l'élément t[i]. La variable cum_sum_i contient donc maintenant \(\sum_{j=0}^{i} t[j]\). La dernière instruction de la boucle est d'incrémenter la variable i d'une unité. On retrouve donc exactement l'invariant spécifié plus haut.

Par hypothèse, au début de la boucle, cum_sum_i contient la somme des i premiers éléments de t. Cette valeur est mise à jour en y ajoutant l'élément t[i+1]. La variable cum_sum_i contient donc maintenant \(\sum_{j=0}^{i} t[j]\). La dernière instruction de la boucle est d'incrémenter la variable i d'une unité. On retrouve donc exactement l'invariant spécifié plus haut.

Par hypothèse, chacun des i premiers élément du tableau t_cum contient la somme cumulée attendue. Ce tableau est mis à jour en y ajoutant, à l'indice i-1, la nouvelle valeur de cum_sum_i. La variable t_cum respecte donc la propriété suivante : \(\forall j \in \{0:(i-1)\} \colon \mathit{t\_cum}[j] = \sum_{k=0}^{j} t[k]\). La dernière instruction de la boucle est d'incrémenter la variable i d'une unité. On retrouve donc exactement l'invariant spécifié plus haut.

Par hypothèse, chacun des i premiers élément du tableau t_cum contient la somme cumulée attendue. Ce tableau est mis à jour en y ajoutant, à l'indice i-1, la nouvelle valeur de cum_sum_i. La variable t_cum respecte donc la propriété suivante : \(\forall j \in \{0:i\} \colon \mathit{t\_cum}[j] = \sum_{k=0}^{j} t[k]\). La dernière instruction de la boucle est d'incrémenter la variable i d'une unité. On retrouve donc exactement l'invariant spécifié plus haut.

Question 4: Condition de terminaison

Lorsque la condition de terminaison est atteinte, l'invariant définit la post-condition.

Sélectionnez, parmi les propositions suivantes, celle qui correspond à la condition d'arrêt de la boucle.

t_cum[i] \(\neq 0\)

Le tableau t_cum est complété selon la post-condition

i \(= \text{len}(t)+1\)

i \(= 0\)

cum_sum_i \(= \sum_{j=0}^{i} t[i]\)

i \(= n\)

i \(= \text{len}(t)\)

Question 5: Preuve

Si l'on utilise la condition d'arrêt pour mettre à jour l'invariant, la correction de la fonction est prouvée.

Sélectionnez, parmi les propositions suivantes, celle(s) qui permet(tent) de prouver directement que la fonction est correcte.

Étant donné l'invariant et la condition d'arrêt, tous les éléments de t_cum contiennent la somme cumulée attendue

Étant donné l'invariant et la condition d'arrêt, la boucle while de la fonction ne sera pas infinie

Étant donné l'invariant et la condition d'arrêt, la variable cum_sum_i contient la somme de tous les éléments de t

Auteur(s)	Vincent Branders, Pierre Dupont
Date limite	22/04/2026 14:00:00
Limite de soumission	Pas de limite

Informations

Se connecter