Correction

Définitions

On se demande si un algorithme – ou, cela revient au même, une fonction – est correct. C'est à dire que l'on veut savoir si l'algorithme fait bien ce qu'il est censé faire et dans quelles conditions il fonctionne correctement.

Précondition

Il s'agit d'un condition portant sur les entrées. Pour que l'algorithme fonctionne correctement, il faut que les préconditions soient respectées.

Postcondition

Ce sont les conditions que nous voulons voir réalisées à la fin de l'exécution de l'algorithme. C'est en vérifiant que les postconditions sont respectées que l'on pourra juger que l'algorithme a fait ce qu'il devait.

Terminaison

On veut que l'algorithme se termine, c'est à dire que son temps d'exécution soit fini. En pratique, on a besoin que ce temps ne soit pas trop long. En théorie, il suffit que ce temps soit fini, même s'il est très grand. Un algorithme termine si son temps d'exécution est fini chaque fois que les préconditions sont vérifiées.

Correction

On dira qu'un algorithme (ou fonction) est correct s'il termine ET que préconditions $\Rightarrow$ postconditions.

Exemple

Je considère une fonction solve(A:int) → int qui renvoie le plus petit entier N tel que N**3 >= A.

def solve(A:int) -> int:
    '''
    renvoie le plus petit entier N tel que N**3 >= A
    '''
    n = 0
    while n**3 < A:
        n += 1
    return n

Terminaison

Cette fonction contient une boucle while. Il faut regarder ces boucles avec soin car elles sont potentiellement illimités.

Ici, n augmente de 1 à chaque boucle, donc n**3 augmente d'au moins 1 à chaque boucle, et donc n**3 finira par dépasser A.

La fonction termine donc.

Correction

On a déjà vérifié que la fonction termine.

Fait-elle ce qu'elle doit ?

Non ! En effet, si A = -10, la fonction renvoie 0 alors que la réponse aurait dû être -2.

La fonction a été écrite en supposant implicitement que A serait positif. Si A >= 0, on n'a plus de problème. Il faut faire attention à ces implicites. Les préconditions sont là justement pour expliciter.

On ajoute donc la précondition : A >= 0. Réécrivons la fonction :

def solve(A:int) -> int:
    '''
    A entier positif
    renvoie le plus petit entier N tel que N**3 >= A
    '''
    n = 0
    while n**3 < A:
        n += 1
    return n

La précondition a été écrite dans le commentaire. Dans certains cas, cela peut suffire. Mais rien n'empêche ici de demander :

>>> solve(-10)
0

La précondition écrite dans le commentaire n'est qu'informative et n'interdit pas un mauvais usage de la fonction.

On peut être plus contraignant :

def solve(A:int) -> int:
    '''
    A entier positif
    renvoie le plus petit entier N tel que N**3 >= A
    '''
    assert A >= 0
    n = 0
    while n**3 < A:
        n += 1
    return n

assert énonce une condition qui doit être valide. Si elle ne l'est pas, l'exécution s'interrompt sur une erreur.

Avec la précondition A >= 0, la fonction est correcte.

La commande assert a d'autres usages :

pour les tests : vérifier les fonctions sur des cas connus d'avance pour s'assurer qu'elles fournissent les bons résultats,
pour la maintenance : certains environnement de programmation comme VSCode sont capable de détecter les assert et de s'en servir pour vérifier la cohérence de l'ensemble. Ainsi, si on a affirmé par assert que telle variable devait être entière mais qu'ailleurs on écrit un float dans cette variable, l'environnement nous préviendra de l'incohérence.