Worldlex Wiki informatique théorique , un algorithme est correct par rapport à une spécification s'il se comporte comme spécifié. La correction fonctionnelle , qui se réfère au comportement entrée-sortie de l'algorithme, est la plus étudiée : pour chaque entrée, il produit une sortie satisfaisant la spécification.
Dans ce cadre, la correction partielle , qui exige que toute réponse renvoyée soit correcte, se distingue de la correction totale , qui exige en outre qu'une réponse soit finalement renvoyée, c'est-à-dire que l'algorithme se termine. Par conséquent, pour prouver la correction totale d'un programme, il suffit de prouver sa correction partielle et sa terminaison. Ce dernier type de preuve ( preuve de terminaison ) ne peut jamais être entièrement automatisé, car le problème de l'arrêt est indécidable .
| Programme C partiellement correct pour trouver le plus petit nombre parfait impair ; sa correction totale est inconnue en 2023. |
entiers positifs (1, 2, 3, …) pour voir si l'on peut trouver un nombre parfait impair est assez simple à écrire et constitue un programme partiellement correct qui trouverait un nombre parfait impair, s'il existe (voir encadré). Cependant, affirmer que ce programme est totalement correct (c'est-à-dire qu'il trouvera un tel nombre et s'arrêtera) reviendrait à affirmer qu'un nombre parfait impair existe réellement, ce qui n'est actuellement pas connu en théorie des nombres . La démonstration devrait être mathématique, en supposant que l'algorithme et sa spécification soient formellement définis. En particulier, il ne s'agit pas d'une assertion de correction pour un programme donné implémentant l'algorithme sur une machine donnée. Cela impliquerait des considérations telles que les limitations de la mémoire de l'ordinateur . Un résultat fondamental de la théorie de la démonstration , la correspondance de Curry-Howard , établit qu'une preuve de correction fonctionnelle en logique constructive correspond à un certain programme dans le lambda-calcul . La conversion d'une preuve de cette manière est appelée extraction de programme . La logique de Hoare est un système formel spécifique permettant de raisonner rigoureusement sur la correction des programmes informatiques. Elle utilise des techniques axiomatiques pour définir la sémantique des langages de programmation et argumenter sur la correction des programmes au moyen d'assertions appelées triplets de Hoare. Les tests logiciels désignent toute activité visant à évaluer un attribut ou une capacité d'un programme ou d'un système et à vérifier qu'il répond aux exigences. Bien que cruciaux pour la qualité des logiciels et largement utilisés par les programmeurs et les testeurs, les tests logiciels restent encore un art en raison d'une compréhension limitée des principes du logiciel. La difficulté des tests logiciels provient de la complexité même des logiciels : il est impossible de tester complètement un programme de complexité modérée. Les tests ne se limitent pas au débogage. Leur objectif peut être l'assurance qualité, la vérification et la validation, ou encore l'estimation de la fiabilité. Les tests peuvent également servir de métrique générique. Les tests de correction et les tests de fiabilité constituent deux domaines majeurs des tests. Les tests logiciels représentent un compromis entre budget, temps et qualité. |