Introduction
Quand on écrit une fonction, il ne suffit pas de coder les instructions : il faut aussi décrire clairement ce qu’elle est censée faire. Cette description permet à d’autres programmeurs (ou à soi-même plus tard) de comprendre comment utiliser la fonction sans forcément lire son code en détail. En algorithmique, on appelle cela la spécification d’une fonction. Elle précise les conditions nécessaires à son exécution (les préconditions) et ce que la fonction garantit en sortie (les postconditions). Pour vérifier que ces règles sont respectées, on peut utiliser des assertions, qui servent de garde-fous pendant l’exécution. Cette démarche rapproche l’informatique d’une discipline scientifique rigoureuse, où l’on prouve que les résultats obtenus correspondent bien à ce qui est attendu.
Spécifier une fonction : préconditions et postconditions
La spécification d’une fonction décrit son comportement attendu, indépendamment de son implémentation. Elle se compose généralement de deux parties :
Les préconditions : elles indiquent les conditions que doivent respecter les arguments pour que la fonction fonctionne correctement.
Exemple : une fonction qui calcule la racine carrée d’un nombre suppose que l’argument est positif.
Les postconditions : elles expriment ce que la fonction garantit après son exécution, autrement dit la relation entre les données en entrée et les résultats en sortie.
Exemple : une fonction racine_carrée renvoie un nombre x tel que x² soit égal à l’argument, à une approximation près.
En Python, cette spécification peut être rédigée en commentaire au-dessus de la fonction, afin de documenter son usage.
À retenir
La spécification d’une fonction indique ce que la fonction doit faire, et non comment elle le fait. Elle repose sur des préconditions et des postconditions.
Les assertions : vérifier les conditions dans le code
Une assertion est une instruction spéciale qui vérifie qu’une condition est vraie pendant l’exécution du programme. Si la condition est fausse, le programme s’arrête avec une erreur. Les assertions permettent de vérifier concrètement que les préconditions et postconditions sont respectées.
Exemple : reprenons la fonction racine carrée. On peut vérifier que l’argument est valide et que le résultat correspond bien à la postcondition.
Si l’utilisateur appelle `racine_carree(-4)`, l’assertion de précondition échoue immédiatement et évite un calcul incorrect. Les assertions jouent donc le rôle de garde-fous, surtout pendant la phase de mise au point d’un programme.
À retenir
Les assertions permettent de vérifier automatiquement les préconditions et postconditions d’une fonction. Elles facilitent la détection des erreurs dès l’exécution.
Exemple concret : une fonction de recherche
Imaginons une fonction qui recherche l’indice d’un élément dans une liste.
Ici :
La précondition est que l’utilisateur fournisse bien une liste de nombres.
La postcondition garantit que si la fonction renvoie un indice i, alors `tableau[i]` est bien égal à la valeur recherchée.
Les assertions insérées dans le code aident à vérifier que la promesse faite par la spécification est tenue.
À retenir
Spécifier une fonction et utiliser des assertions permet de passer d’une simple intuition sur le programme à une véritable preuve de correction partielle : on garantit que, si la fonction s’exécute, elle respecte ce qui est annoncé.
Conclusion
Décrire ce que fait une fonction est aussi important que son code. La spécification, à travers préconditions et postconditions, permet de communiquer clairement son rôle et ses garanties. Les assertions, quant à elles, constituent un moyen simple de vérifier que ces règles sont respectées lors de l’exécution. En combinant ces deux outils, on fait un pas vers une programmation plus fiable, où la correction ne repose pas uniquement sur des tests, mais sur des principes formels. Dans la suite du programme, cette rigueur sera essentielle pour analyser la validité des algorithmes étudiés.
