INGIniousFormalisation 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.