Rectitude (informatique) - Correctness (computer science)

En informatique théorique , un algorithme est correct par rapport à une spécification s'il se comporte comme spécifié. Le mieux exploré est l' exactitude fonctionnelle , qui fait référence au comportement d'entrée-sortie de l'algorithme (c'est-à-dire que pour chaque entrée, il produit une sortie satisfaisant la spécification).

Au sein de cette dernière notion, l'exactitude partielle , exigeant que si une réponse est renvoyée, elle soit correcte, se distingue de l'exactitude totale , qui exige en outre qu'une réponse soit finalement renvoyée, c'est-à-dire que l'algorithme se termine. Corrélativement, pour prouver l'exactitude totale d'un programme, il suffit de prouver son exactitude partielle et sa terminaison. Ce dernier type de preuve (preuve de terminaison ) ne peut jamais être entièrement automatisé, car le problème d'arrêt est indécidable .

Programme C partiellement correct pour trouver
le nombre parfait le moins impair,
son exactitude totale est inconnue à partir de 2021
// return the sum of proper divisors of n
static int divisorSum(int n) {
   int i, sum = 0;
   for (i=1; i<n; ++i)
      if (n % i == 0)
         sum += i;
   return sum;
}
// return the least odd perfect number
int leastPerfectNumber(void) {
   int n;
   for (n=1; ; n+=2)
      if (n == divisorSum(n))
         return n;
}

Par exemple, en cherchant successivement dans les nombres entiers 1, 2, 3, … pour voir si nous pouvons trouver un exemple d'un phénomène - disons un nombre parfait impair - il est assez facile d'écrire un programme partiellement correct (voir encadré). Mais dire que ce programme est totalement correct reviendrait à affirmer quelque chose qui n'est actuellement pas connu en théorie des nombres .

Une preuve devrait être une preuve mathématique, en supposant que l'algorithme et la spécification soient donnés formellement. En particulier, on ne s'attend pas à ce qu'il s'agisse d'une assertion d'exactitude pour un programme donné mettant en œuvre 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 profond de la théorie de la preuve , la correspondance Curry-Howard , indique qu'une preuve d'exactitude fonctionnelle en logique constructive correspond à un certain programme du lambda calcul . La conversion d'une preuve de cette manière est appelée extraction de programme .

La logique hoare est un système formel spécifique permettant de raisonner rigoureusement sur l'exactitude des programmes informatiques. Il utilise des techniques axiomatiques pour définir la sémantique du langage de programmation et argumenter sur l'exactitude des programmes au moyen d'assertions connues sous le nom de triplets de Hoare.

Les tests de logiciels sont toute activité visant à évaluer un attribut ou une capacité d'un programme ou d'un système et de déterminer qu'il répond aux résultats requis. Bien qu'essentiels à la qualité des logiciels et largement déployés par les programmeurs et les testeurs, les tests logiciels restent un art, en raison d'une compréhension limitée des principes des logiciels. La difficulté des tests logiciels vient de la complexité des logiciels : on ne peut pas tester complètement un programme avec une complexité modérée. Le test est plus qu'un simple débogage. Le but des tests peut être l'assurance qualité, la vérification et la validation, ou l'estimation de la fiabilité. Les tests peuvent également être utilisés comme métrique générique. Les tests d'exactitude et les tests de fiabilité sont deux domaines principaux de test. Les tests de logiciels sont un compromis entre le budget, le temps et la qualité.

Voir également

Remarques

Les références