Lista de cursos Registro Entrar

Informações

Prazo de entrega Sem prazo
Limite de submissão No limitation

Entrar

Entrar

[3.0] L'état d'un programme

Formalisation de l'état d'un programme

Pour prouver qu'un programme est correct, il est d'abord important de formaliser les données qu'il manipule, c'est à dire l’état de l’exécution du programme. Cela se fait grâce à une assertion qui est juste une proposition que l'on soutient comme vraie et qui est formalisée par les mathématiques.

Exemple

Si on prend le programme ci-dessous :

int main(void) {
    int x = 4;
    return 0;
}

On peut savoir qu'au début de l'exécution du programme, avant l'instruction int x = 4;, il n'y a pas de variables initialisées et donc l'état est vide, ce qu'on note \(()\). Par contre, après l'exécution de l'instruction, on sait qu'il y a x qui vaut 4 et donc l'état devient \((x = 4)\).

Formalisation de l'exécution d'une instruction

Pour formaliser l'exécution et la correction partielle d'une instruction, nous allons utiliser ce qu'on appelle un triplet de Hoare, qui se note souvent grâce à l'assertion \(\{P\} S \{Q\}\). Vous pouvez lire cela comme si P est vraie avant l’exécution de S et si l’exécution de S se termine alors Q est vraie après l’exécution de S. Dans le cadre d'un triplet de Hoare, \(P\) est ce qu'on appelle la précondition et \(Q\) la postcondition.

Exemple

Si l'on reprend le programme d'au-dessus, le triplet de Hoare correspondant à l'exécution de l'instruction int x = 4; serait \(\{\}\ int\ x\ =\ 4;\ \{x = 4\}\). Ce triplet peut se lire comme si l'état est vide avant l’exécution de int x = 4; et si l’exécution de int x = 4; se termine alors x vaut 4 après l’exécution de int x = 4;.

L'invariant

L'invariant d'une boucle est une assertion qui est vraie juste avant l’entrée dans la boucle et à la fin de l’exécution du corps de la boucle. En fonction de ce que l'on cherche à prouver, il peut exister plusieurs invariants valides pour une même boucle qui seront juste plus ou moins précis.

ATTENTION!
L'invariant doit donc être vrai avant et après une itération de la boucle mais pendant l'itération de la boucle, c'est autorisé de ne pas respecter l'invariant temporairement.
Information
Il existe aussi des invariants sur les structures de données. Ce sont des assertions qui doivent à la fin des fonctions qui créent ces structures de données et qui doivent être vraies avant et après l'appel des fonctions qui manipulent ces structures de données. C'est ce qui est appelé invariant de représentation dans le cours Conception et programmation orientée objet.
Questão 1:

Si on part de l'état \((x = 2)\), quel sera l'état du programme le plus précis après l'exécution de l'instruction suivante :

int y = 4;
Questão 2:

Si on part de l'état \((x = 2)\), quel sera l'état du programme le plus précis après l'exécution de l'instruction suivante :

int y = x - 2;
Questão 3:

Si on part de l'état \((i = 0)\), quel sera l'état du programme le plus précis après l'exécution de l'instruction suivante :

i = i + 1;
Questão 4:

Si on part de l'état \((x = 2)\), quels sont les états corrects du programme après l'exécution de l'instruction suivante :

int y = x - 2;
Questão 5:

Si on part de l'état \((i > 0)\), quel sera l'état du programme après l'exécution de l'instruction suivante :

i = i + 1;
Questão 6:

Soit le triplet suivant :

\(\{a \geq 5\}\ int\ b\ =\ a\ +\ 3\ \{ Q \}\)

Quel est la postcondition \(Q\) la plus précise ?

Questão 7:

Soit le triplet suivant :

\(\{tab[0] = 1 \land tab[1] = 2 \land tab[2] = 3\}\ tab[1]\ =\ 4;\ \{ Q \}\)

Quel est la postcondition \(Q\) la plus précise ?

Questão 8:

Soit le triplet suivant :

\(\{tab[0] = 1 \land tab[1] = 2 \land tab[2] = 3\}\ tab[0]\ =\ tab[0]\ +\ 1;\ \{ Q \}\)

Quels sont les postconditions \(Q\) correctes ?

Questão 9:

Soit le programme ci-dessous :

int i = 0;

while (i < n) {
    i = i + 1;
}

Quel est l'invariant le plus précis ?

Questão 10:

Soit le programme ci-dessous :

int somme = 0;
int i = 0;
while (i < n) {
    somme = somme + i;
    i = i + 1;
}

Quel est l'invariant le plus précis ?