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

<WRAP tip>**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.
</WRAP>

<WRAP tip>**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.
</WRAP>

<WRAP tip>**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.
</WRAP>

<WRAP tip>**Correction**

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

===== Exemple =====

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

<code python>
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
</code>

=== 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 ?

<WRAP box>**Non !** En effet, si ''A = -10'', la fonction renvoie ''0'' alors que la réponse aurait dû être ''-2''.</WRAP>

<WRAP important>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.</WRAP>

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

<code python>
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
</code>

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

<code python>
>>> solve(-10)
0
</code>

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 :

<code python>
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
</code>

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

<WRAP box>Avec la précondition ''A >= 0'', la fonction est correcte.</WRAP>

<WRAP tip>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 [[https://code.visualstudio.com/|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.
</WRAP>