Affirmation (développement logiciel) - Assertion (software development)

Cet article concerne le concept de programmation informatique. Pour les assertions dans le contexte de la norme ouverte SAML ( Security Assertion Markup Language ), consultez Security Assertion Markup Language § Assertions .

En programmation informatique , en particulier lors de l'utilisation du paradigme de la programmation impérative , une assertion est un prédicat (une fonction à valeur booléenne sur l' espace d'état , généralement exprimée sous la forme d'une proposition logique utilisant les variables d'un programme) connecté à un point du programme, qui doit toujours avoir la valeur true à ce stade de l'exécution du code. Les assertions peuvent aider un programmeur à lire le code, aider un compilateur à le compiler ou aider le programme à détecter ses propres défauts.

Pour ces derniers, certains programmes vérifient les assertions en évaluant réellement le prédicat lors de leur exécution. Ensuite, si ce n'est pas vrai - un échec d'assertion - le programme se considère comme étant cassé et typiquement se bloque délibérément ou lève une exception d' échec d'assertion .

Des détails

Le code suivant contient deux assertions, x > 0et x > 1, et elles sont en effet vraies aux points indiqués lors de l'exécution : 

x = 1;
assert x > 0;
x++;
assert x > 1;

Les programmeurs peuvent utiliser des assertions pour aider à spécifier des programmes et à raisonner sur l'exactitude des programmes. Par exemple, une condition préalable — une assertion placée au début d'une section de code — détermine l'ensemble d'états sous lesquels le programmeur s'attend à ce que le code s'exécute. Une postcondition — placée à la fin — décrit l'état attendu à la fin de l'exécution. Par exemple : x > 0 { x++ } x > 1.

L'exemple ci-dessus utilise la notation pour inclure les affirmations utilisées par CAR Hoare dans son article de 1969. Cette notation ne peut pas être utilisée dans les langages de programmation traditionnels existants. Cependant, les programmeurs peuvent inclure des assertions non vérifiées en utilisant la fonction de commentaire de leur langage de programmation. Par exemple, en C : 

x = 5;
x = x + 1;
// {x > 1}

Les accolades incluses dans le commentaire permettent de distinguer cette utilisation d'un commentaire des autres utilisations.

Les bibliothèques peuvent également fournir des fonctionnalités d'assertion. Par exemple, en C en utilisant la glibc avec le support C99 : 

#include <assert.h>

int f(void)
{
    int x = 5;
    x = x + 1;
    assert(x > 1);
}

Plusieurs langages de programmation modernes incluent des assertions vérifiées - des déclarations qui sont vérifiées au moment de l' exécution ou parfois de manière statique. Si une assertion est évaluée à false au moment de l'exécution, un échec d'assertion se produit, ce qui entraîne généralement l'abandon de l'exécution. Cela attire l'attention sur l'emplacement auquel l'incohérence logique est détectée et peut être préférable au comportement qui en résulterait autrement.

L'utilisation d'assertions aide le programmeur à concevoir, développer et raisonner un programme.

Usage

Dans des langages comme Eiffel , les assertions font partie du processus de conception ; d'autres langages, tels que C et Java , ne les utilisent que pour vérifier les hypothèses lors de l'exécution. Dans les deux cas, leur validité peut être vérifiée au moment de l'exécution mais peut généralement être également supprimée.

Assertions en conception par contrat

Les assertions peuvent fonctionner comme une forme de documentation : elles peuvent décrire l'état que le code s'attend à trouver avant de s'exécuter (ses conditions préalables ) et l'état dans lequel le code s'attend à ce qu'il soit à la fin de son exécution ( postconditions ) ; ils peuvent aussi spécifier les invariants d'une classe . Eiffel intègre de telles assertions dans le langage et les extrait automatiquement pour documenter la classe. Ceci constitue une partie importante de la méthode de conception par contrat .

Cette approche est également utile dans les langages qui ne la supportent pas explicitement : l'avantage d'utiliser des déclarations d'assertion plutôt que des assertions dans les commentaires est que le programme peut vérifier les assertions à chaque fois qu'il s'exécute ; si l'assertion ne tient plus, une erreur peut être signalée. Cela empêche le code de se désynchroniser avec les assertions.

Assertions pour la vérification à l'exécution

Une assertion peut être utilisée pour vérifier qu'une hypothèse faite par le programmeur lors de la mise en œuvre du programme reste valide lorsque le programme est exécuté. Par exemple, considérons le code Java suivant : 

 int total = countNumberOfUsers();
 if (total % 2 == 0) {
     // total is even
 } else {
     // total is odd and non-negative
     assert total % 2 == 1;
 }

En Java , %est l' opérateur reste ( modulo ), et en Java, si son premier opérande est négatif, le résultat peut aussi être négatif (contrairement au modulo utilisé en mathématiques). Ici, le programmeur a supposé que totalc'était non négatif, de sorte que le reste d'une division avec 2 sera toujours 0 ou 1. L'assertion rend cette hypothèse explicite : si countNumberOfUsersrenvoie une valeur négative, le programme peut avoir un bogue.

Un avantage majeur de cette technique est que lorsqu'une erreur se produit, elle est détectée immédiatement et directement, plutôt que plus tard par des effets souvent obscurs. Étant donné qu'un échec d'assertion signale généralement l'emplacement du code, on peut souvent localiser l'erreur sans débogage supplémentaire.

Des assertions sont également parfois placées à des points que l'exécution n'est pas censée atteindre. Par exemple, les assertions peuvent être placées dans la defaultclause de l' switchinstruction dans des langages tels que C , C++ et Java . Tout cas que le programmeur ne traite pas intentionnellement générera une erreur et le programme abandonnera plutôt que de continuer silencieusement dans un état erroné. En D , une telle assertion est ajoutée automatiquement lorsqu'une switchinstruction ne contient pas de defaultclause.

En Java , les assertions font partie du langage depuis la version 1.4. Les échecs d'assertion entraînent le déclenchement d'un AssertionErrorlorsque le programme est exécuté avec les indicateurs appropriés, sans lesquels les instructions d'assertion sont ignorées. En C , ils sont ajoutés par l'en-tête standard assert.hdéfini comme une macro qui signale une erreur en cas d'échec, terminant généralement le programme. En C++ , les en - têtes et fournissent la macro. assert (assertion) assert.hcassertassert

Le danger des assertions est qu'elles peuvent provoquer des effets secondaires en modifiant les données de la mémoire ou en modifiant la synchronisation des threads. Les assertions doivent être implémentées avec soin afin qu'elles ne provoquent aucun effet secondaire sur le code du programme.

Les constructions d'assertion dans un langage permettent un développement simple piloté par les tests (TDD) sans l'utilisation d'une bibliothèque tierce.

Assertions au cours du cycle de développement

Au cours du cycle de développement , le programmeur exécutera généralement le programme avec les assertions activées. Lorsqu'un échec d'assertion se produit, le programmeur est immédiatement informé du problème. De nombreuses implémentations d'assertion arrêteront également l'exécution du programme : c'est utile, car si le programme continuait à s'exécuter après qu'une violation d'assertion se soit produite, cela pourrait corrompre son état et rendre la cause du problème plus difficile à localiser. En utilisant les informations fournies par l'échec de l'assertion (telles que l'emplacement de l'échec et peut-être une trace de pile , ou même l'état complet du programme si l'environnement prend en charge les vidages de mémoire ou si le programme s'exécute dans un débogueur ), le programmeur peut généralement corriger le problème. Ainsi, les assertions fournissent un outil très puissant pour le débogage.

Assertions en environnement de production

Lorsqu'un programme est déployé en production , les assertions sont généralement désactivées, pour éviter toute surcharge ou effet secondaire qu'elles peuvent avoir. Dans certains cas, les assertions sont complètement absentes du code déployé, comme dans les assertions C/C++ via des macros. Dans d'autres cas, tels que Java, les assertions sont présentes dans le code déployé et peuvent être activées sur le terrain pour le débogage.

Les assertions peuvent également être utilisées pour promettre au compilateur qu'une condition limite donnée n'est pas réellement accessible, permettant ainsi certaines optimisations qui ne seraient pas possibles autrement. Dans ce cas, la désactivation des assertions pourrait en fait réduire les performances.

Assertions statiques

Les assertions vérifiées au moment de la compilation sont appelées assertions statiques.

Les assertions statiques sont particulièrement utiles dans la métaprogrammation de modèles de compilation , mais peuvent également être utilisées dans des langages de bas niveau comme C en introduisant du code illégal si (et seulement si) l'assertion échoue. C11 et C++11 prennent en charge les assertions statiques directement via static_assert. Dans les versions antérieures du C, une assertion statique peut être implémentée, par exemple, comme ceci : 

#define SASSERT(pred) switch(0){case 0:case pred:;}

SASSERT( BOOLEAN CONDITION );

Si la (BOOLEAN CONDITION)partie est évaluée à faux, le code ci-dessus ne sera pas compilé car le compilateur n'autorisera pas deux étiquettes de cas avec la même constante. L'expression booléenne doit être une valeur constante au moment de la compilation, par exemple serait une expression valide dans ce contexte. Cette construction ne fonctionne pas au niveau du fichier (c'est-à-dire pas à l'intérieur d'une fonction), et doit donc être encapsulée dans une fonction. (sizeof(int)==4)

Une autre façon populaire d'implémenter des assertions en C est : 

static char const static_assertion[ (BOOLEAN CONDITION)
                                    ? 1 : -1
                                  ] = {'!'};

Si la (BOOLEAN CONDITION)partie est évaluée à false, le code ci-dessus ne sera pas compilé car les tableaux peuvent ne pas avoir une longueur négative. Si en fait le compilateur autorise une longueur négative, alors l'octet d'initialisation (la '!'partie) devrait faire se plaindre même de tels compilateurs trop indulgents. L'expression booléenne doit être une valeur constante au moment de la compilation, par exemple (sizeof(int) == 4)serait une expression valide dans ce contexte.

Ces deux méthodes nécessitent une méthode de construction de noms uniques. Les compilateurs modernes prennent en charge une __COUNTER__définition de préprocesseur qui facilite la construction de noms uniques, en renvoyant des nombres croissants de manière monotone pour chaque unité de compilation.

D fournit des assertions statiques via l'utilisation de static assert.

Désactivation des assertions

La plupart des langages permettent d'activer ou de désactiver les assertions globalement, et parfois indépendamment. Les assertions sont souvent activées pendant le développement et désactivées pendant les tests finaux et lors de la mise à disposition du client. Ne pas vérifier les assertions évite le coût de l'évaluation des assertions tout en produisant (en supposant que les assertions sont exemptes d' effets secondaires ) le même résultat dans des conditions normales. Dans des conditions anormales, la désactivation de la vérification des assertions peut signifier qu'un programme qui aurait été interrompu continuera à s'exécuter. C'est parfois préférable.

Certains langages, notamment C et C++ , peuvent supprimer complètement les assertions au moment de la compilation à l'aide du préprocesseur . Java nécessite qu'une option soit transmise au moteur d'exécution afin d'activer les assertions. En l'absence d'option, les assertions sont contournées, mais elles restent toujours dans le code à moins qu'elles ne soient optimisées par un compilateur JIT au moment de l'exécution ou exclues par une if (false)condition au moment de la compilation, elles n'ont donc pas besoin d'un espace d'exécution ou d'un coût en temps en Java Soit.

Les programmeurs peuvent intégrer dans leur code des vérifications qui sont toujours actives en contournant ou en manipulant les mécanismes normaux de vérification d'assertion du langage.

Comparaison avec la gestion des erreurs

Les assertions sont distinctes de la gestion des erreurs de routine. Les assertions documentent des situations logiquement impossibles et découvrent des erreurs de programmation : si l'impossible se produit, alors quelque chose de fondamental ne va clairement pas avec le programme. Ceci est différent de la gestion des erreurs : la plupart des conditions d'erreur sont possibles, bien que certaines soient extrêmement improbables dans la pratique. L'utilisation d'assertions comme mécanisme de gestion d'erreurs à usage général n'est pas judicieuse : les assertions ne permettent pas de récupérer des erreurs ; un échec d'assertion arrêtera normalement brutalement l'exécution du programme ; et les assertions sont souvent désactivées dans le code de production. Les assertions n'affichent pas non plus de message d'erreur convivial.

Prenons l'exemple suivant d'utilisation d'une assertion pour gérer une erreur : 

  int *ptr = malloc(sizeof(int) * 10);
  assert(ptr);
  // use ptr
  ...

Ici, le programmeur sait qu'il mallocrenverra un NULLpointeur si la mémoire n'est pas allouée. C'est possible : le système d'exploitation ne garantit pas que chaque appel à mallocaboutira. Si une erreur de mémoire insuffisante se produit, le programme s'arrêtera immédiatement. Sans l'assertion, le programme continuerait à s'exécuter jusqu'à ce qu'il ptrsoit déréférencé, et peut-être plus longtemps, en fonction du matériel spécifique utilisé. Tant que les assertions ne sont pas désactivées, une sortie immédiate est assurée. Mais si un échec gracieux est souhaité, le programme doit gérer l'échec. Par exemple, un serveur peut avoir plusieurs clients, ou peut contenir des ressources qui ne seront pas libérées proprement, ou il peut avoir des modifications non validées à écrire dans une banque de données. Dans de tels cas, il vaut mieux échouer une seule transaction que d'abandonner brusquement.

Une autre erreur est de s'appuyer sur les effets secondaires des expressions utilisées comme arguments d'une assertion. Il faut toujours garder à l'esprit que les affirmations peuvent ne pas être exécutées du tout, car leur seul but est de vérifier qu'une condition qui devrait toujours être vraie est en fait vraie. Par conséquent, si le programme est considéré comme exempt d'erreurs et libéré, les assertions peuvent être désactivées et ne seront plus évaluées.

Considérons une autre version de l'exemple précédent : 

  int *ptr;
  // Statement below fails if malloc() returns NULL,
  // but is not executed at all when compiling with -NDEBUG!
  assert(ptr = malloc(sizeof(int) * 10));
  // use ptr: ptr isn't initialised when compiling with -NDEBUG!
  ...

Cela peut sembler un moyen intelligent d'affecter la valeur de retour de mallocto ptret de vérifier si c'est NULLen une seule étape, mais l' mallocappel et l'affectation à ptrest un effet secondaire de l'évaluation de l'expression qui forme la assertcondition. Lorsque le NDEBUGparamètre est passé au compilateur, comme lorsque le programme est considéré comme sans erreur et libéré, l' assert()instruction est supprimée, donc malloc()n'est pas appelée, ce qui rend ptrnon initialisé. Cela pourrait potentiellement entraîner une erreur de segmentation ou une erreur de pointeur null similaire beaucoup plus loin dans l'exécution du programme, provoquant des bogues qui peuvent être sporadiques et/ou difficiles à localiser. Les programmeurs utilisent parfois une définition VERIFY(X) similaire pour atténuer ce problème.

Les compilateurs modernes peuvent émettre un avertissement lorsqu'ils rencontrent le code ci-dessus.

Histoire

Dans les rapports de 1947 de von Neumann et Goldstine sur leur conception de la machine IAS , ils décrivaient des algorithmes utilisant une première version des organigrammes , dans lesquels ils incluaient des affirmations : « Il peut être vrai que chaque fois que C atteint un certain point dans le flux diagramme, une ou plusieurs variables liées posséderont nécessairement certaines valeurs spécifiées, ou posséderont certaines propriétés, ou satisferont certaines propriétés les unes avec les autres. De plus, nous pourrons, à un tel point, indiquer la validité de ces limitations. Pour cette raison, nous noterons chaque domaine dans lequel la validité de telles limitations est affirmée, par une boîte spéciale, que nous appelons une boîte d'assertion. »

La méthode assertive pour prouver l'exactitude des programmes a été préconisée par Alan Turing . Dans une conférence « Checking a Large Routine » à Cambridge, le 24 juin 1949, Turing a suggéré : « Comment peut-on vérifier une grande routine dans le sens de s'assurer qu'elle est correcte ? tâche, le programmeur doit faire un certain nombre d' affirmations précises qui peuvent être vérifiées individuellement, et à partir desquelles l'exactitude de l'ensemble du programme découle facilement".

Voir également

Les références

Liens externes