Expression booléenne
5.1 Spécifications basées sur les états
Les spécifications basées sur les états décrivent les systèmes logiciels en termes d’états et d’effets des opérations sur les états. De telles spécifications sont supportées par plusieurs langages de spécification, que nous avons regroupés en deux ensembles : les langages de spécification classiques, tels que Z , B , et VDM , et les langages d’assertion, tels que Eiffel , JML (Java Modeling Language) , et les tables de Peters et Parnas . Alors que les langages de spécification classiques définissent les états et les transitions indépendamment de l’implémentation, les langages d’assertion spécifient les états et les transitions comme des déclarations ou des annotations du programme source.
Les spécifications basées sur les états sont utilisées comme oracles de test en vérifiant la conformité des exécutions de test avec les spécifications. Le problème principal dans la génération d’oracles de test à partir de spécifications basées sur l’état vient des différents niveaux d’abstraction entre les spécifications et les opérations surveillées pendant l’exécution du test ; ainsi, les spécifications des opérations seront traduites dans une forme vérifiable. Les langages de spécification sont généralement assez expressifs pour représenter diverses structures de données et propriétés basées sur l’état, mais leur expressivité complique la traduction en forme exécutable. Souvent, la traduction fait quelques hypothèses simplificatrices, comme la limitation des ensembles infinis, par exemple l’ensemble infini des nombres naturels, et le traitement des éléments non exécutables seulement partiellement et parfois en exigeant une certaine intervention humaine.
Ci-après, nous discutons les principales approches pour traduire les spécifications basées sur l’état dans une forme exécutable. La traduction des spécifications Z, B, et VDM présente les mêmes problèmes liés aux structures de données infinies, aux expressions partiellement définies et aux structures orientées objet. La traduction d’Eiffel, de JML et d’autres langages d’assertion dans une forme vérifiable présente des problèmes similaires mais à un niveau d’abstraction différent. Dans ce qui suit, nous présentons les principales approches pour traduire les spécifications basées sur l’état dans une forme vérifiable en nous référant à Z ; les approches pour d’autres langages sont similaires. Ensuite, nous discutons des problèmes de compilation des assertions en vérifications exécutables en nous référant à Eiffel, JML, et aux tables de Peters et Parnas.
Le compilateur de prédicats de schémas proposé par Mikk compile les spécifications Z en code C. Pour chaque schéma Z, qui est l’unité de base de Z, l’approche génère une fonction C qui évalue les prédicats de schéma en utilisant l’état du programme passé à la fonction comme paramètre. Le code généré évalue les prédicats du schéma avec une stratégie de « force brute » : Étant donné un état, le code remplace essentiellement les expressions par leurs valeurs, évalue les formules du calcul propositionnel en utilisant les tables de vérité, et évalue les quantifications et les constructions d’ensembles en itérant à travers les structures de données. Pour réduire la complexité des fonctions C générées, l’approche propose une étape d’optimisation pour garantir que le code C généré se termine toujours. Afin d’optimiser le code, la technique définit un sous-ensemble « exécutable » du langage Z. Ce sous-ensemble est constitué de prédicats finis, tels que des formules de calcul propositionnel, des quantifications sur des ensembles finis et des constructions d’ensembles basées sur une itération finie. La technique étend l’ensemble des prédicats exécutables avec un ensemble de règles pour transformer les prédicats spéciaux non exécutables qui satisfont certaines conditions en prédicats exécutables sans changer leur sémantique. Par exemple, les deux règles suivantes éliminent les quantificateurs :
où M est un ensemble, la variable x représente un élément de M, et P est un prédicat. L’opérateur -, également connu sous le nom de » tache de notation Z « , signifie » tel que » lorsqu’il est utilisé avec le quantificateur ∃ et » que « , lorsqu’il est utilisé avec le quantificateur ∀. Par exemple, ∃ x : M – P signifie qu’il existe au moins une valeur x dans M telle que le prédicat P est vrai. La condition NotOccur(x, P) indique que x n’est pas une variable libre dans le prédicat P. Bien que l’ensemble M puisse être infini, le compilateur peut toujours compiler des spécifications utilisant des quantificateurs sur M tant que les quantificateurs peuvent être éliminés en appliquant les règles ci-dessus. Pour les fonctions définies par l’utilisateur qui peuvent être introduites par des définitions axiomatiques ou génériques, le compilateur demande à l’utilisateur de fournir le code correspondant. Mikk propose également une solution au problème des spécifications partiellement définies. Il utilise VDM-SL comme forme intermédiaire et le compilateur VDM-SL développé par Schmidt et Hörcher pour traduire les spécifications Z en code C . Lorsqu’elle traite des expressions partiellement définies, c’est-à-dire soit des fonctions ou des relations qui peuvent s’évaluer indéfinies (notées ⊥) lorsqu’elles sont évaluées en dehors de leur domaine de définition, l’approche génère des gestionnaires d’exceptions.
Les extensions orientées objet de Z, comme Object-Z, exacerbent les problèmes. McDonald et al. traduisent les spécifications Ojbect-Z des classes conteneurs en code C++ en trois étapes : optimisation, mappage structurel et traduction des prédicats . Lors de l’étape d’optimisation, ils réorganisent la spécification pour simplifier la traduction ultérieure en plusieurs étapes, notamment en remplaçant les variables constantes par leurs valeurs et en supprimant les variables secondaires et les enrichissements de schéma. Dans l’étape de mappage structurel, ils mappent les structures de la spécification Object-Z à leurs éléments de code correspondants : Les constantes et les variables de la spécification en variables avec des initialisations appropriées, et les types de variables en types primitifs C++ ou en classes correspondantes dans la bibliothèque de la boîte à outils Z utilisée par la technique. Par exemple, ils mappent les types entiers et booléens à int, et le type des ensembles d’entiers à z_set<int >. Ils mappent le schéma d’initialisation à un constructeur, et les schémas d’opération à des fonctions membres, créent une fonction membre spéciale, inv(), pour vérifier l’invariant de classe, et génèrent une classe d’exception pour chaque schéma d’exception.
Dans la traduction du prédicat DeepL, la technique se concentre sur la façon de générer du code pour vérifier l’état du programme, au lieu d’évaluer les prédicats. Par exemple, la traduction empêche la fonction inv() d’appeler toute autre fonction membre, pour éviter la récursion infinie. Dans un constructeur, l’invariant de classe est vérifié à sa sortie.
Richardson et al. se concentrent sur les systèmes critiques en temps, traitent une combinaison de logique Z et de logique d’intervalle temporel, et proposent une traduction des spécifications en oracles de test au moyen d’une interprétation symbolique. L’interprétation symbolique attribue les noms symboliques des spécifications aux entrées du stimulus et aux variables d’état initial, en se référant aux mappages des données et des contrôles. Ensuite, l’interprétation symbolique interprète chaque chemin de contrôle dans les spécifications, c’est-à-dire qu’elle crée une assertion exprimant la condition sur les données de la spécification en fonction de l’état symbolique à chaque point de contrôle de la spécification. Un point de contrôle de spécification est un élément pertinent, tel qu’un événement paramétré, une transition et une opération. Après l’interprétation symbolique de la spécification Z, les informations de l’oracle sont représentées comme une liste de schémas Z pertinents et de leurs assertions correspondantes, qui sont vérifiées si le schéma est invoqué. L’exécution d’un scénario de test fait référence à une entrée de test concrète à partir de laquelle des variables et des événements concrets sont liés à leurs homologues dans la classe de test (chaque classe de test est une partition de l’entrée de test). L’exécution du cas de test produit un profil d’exécution, et les événements concrets et les valeurs des variables contenues dans le profil d’exécution sont mappés au niveau de l’oracle pour vérifier leur cohérence avec les informations de l’oracle.
Les langages d’assertions fusionnent les spécifications avec le code source, ce qui simplifie mais n’élimine pas le problème de traduction. Les assertions sont prises en charge par différents langages et méthodologies. La conception par contrat est un paradigme de conception de logiciels qui postule la conception conjointe du code et des assertions. La conception par contrat a été proposée par Meyer et est entièrement prise en charge par le langage de programmation Eiffel. Contrairement aux langages de spécification générale, comme Z, les spécifications dans Eiffel, appelées contrats, sont intégrées au code source et définissent les obligations et les avantages des composants logiciels qui communiquent via des interfaces bien conçues. Dans les langages supportant les contrats, les obligations et les avantages des clients sont exprimés sous forme de pré et postconditions des fournisseurs de services. Le code source est enrichi d’invariants qui représentent les propriétés d’état qui doivent tenir pendant toute interaction.
Les contrats ont été étendus à de nombreux langages. iContract a été le premier outil à supporter les contrats en Java . Dans iContract, les contrats sont écrits sous forme de commentaires de code avec des balises spéciales. Les contrats supportés par iContract sont des expressions booléennes conformes à la syntaxe Java, à l’exception de quelques extensions syntaxiques qui incluent la quantification universelle (∀), la quantification existentielle (∃), et l’implication (→). Ces extensions sont destinées à simplifier leur traduction en code Java. Par exemple , the syntax of ∀ is forall < Class >< var > in < Enum >< Exp_var >, where < Class > is the type of the variable < var >, which represents an element of < Enum >. A reasonable translation of the ∀ expression is to use a Java loop to iterate over the enumeration < Enum > and evaluate the boolean expression < Exp_var > in each iteration. The existential quantification is translated similarly. An implication expression C implies I can be simply translated into an if statement: « si C alors vérifie I. »
En plus de la simple traduction des expressions booléennes, iContract aborde les questions liées au cycle de vie des objets, à la portée des variables et à l’héritage, la plupart étant spécifiques de la programmation orientée objet. Les règles les plus importantes liées au cycle de vie des objets sont les suivantes :
Dans une construction d’objet, les préconditions doivent être vérifiées au début de la construction, tandis que les invariants et les postconditions ne sont vérifiés que si la construction se termine normalement (sans exceptions).
Pour les invocations normales de méthodes sur les objets, les préconditions et les postconditions sont vérifiées à l’entrée et à la sortie des méthodes invoquées, et les invariants ne sont pas vérifiés pour les méthodes privées.
Dans la destruction d’un objet, aucune vérification n’est requise. Ainsi, aucun code de vérification n’est inséré dans les méthodes finalize().
Les prédicats utilisés dans les postconditions font souvent référence à la fois à la valeur de retour de la méthode et à l' »ancienne » valeur (ou « valeur d’entrée ») de certaines variables. iContract synthétise une pseudo-variable, appelée return, pour représenter la valeur de retour, stocke les valeurs des variables à l’entrée, et les rend accessibles en tant que noms de variables avec le postfixe @pre. Pour les expressions, leurs références d’objets sont stockées directement. iContract autorise les appels aux méthodes membres dans les contrats. Par conséquent, il peut y avoir des récursions potentielles infinies dans la vérification des invariants. Pour résoudre ce problème, iContract garde la trace de la profondeur de récursion pour chaque objet au sein de chaque thread et ne vérifie que les invariants de profondeur 0. Les mécanismes d’extension de type en Java ont plusieurs implications sur la façon dont les contrats des types doivent être gérés. iContract propage les contrats en suivant ces règles :
Les invariants sont conjoints, c’est-à-dire que l’invariant d’un sous-type est la conjonction des invariants de tous ses supertypes.
Les postconditions sont conjointes, c’est-à-dire que la postcondition d’un sous-type est la conjonction des postconditions de tous ses supertypes.
Les préconditions sont disjointes, c’est-à-dire que la précondition d’un sous-type est la disjonction des préconditions de tous ses supertypes.
JML est un langage de spécification comportementale populaire qui prend en charge la conception par contrat en Java . Les contrats JML se présentent sous la forme de commentaires spéciaux en Java. JML exprime les préconditions, les postconditions et les invariants sous forme d’expressions booléennes précédées des mots-clés requires, ensures et invariant, respectivement, et utilise la méthode intégrée \ old(x) pour représenter la valeur de x avant une opération. De manière similaire à la notation ▵ de Z, JML fournit le mot-clé modifies pour indiquer les variables qui sont modifiées dans le corps d’une méthode. En outre, JML traite plusieurs caractéristiques orientées objet, telles que la visibilité et l’héritage.
JML est la base de nombreuses approches de génération d’oracles de test. Bhorkar a proposé une technique pour traduire les contrats JML en assertions Java . Bien que ne supportant que les préconditions, cette technique répond aux problèmes liés aux variables de spécification uniquement, au raffinement, à l’héritage de spécification et à la confidentialité. Comme iContract, cette technique gère l’héritage des contrats en les conjoignant et en les disjoignant en fonction de leurs types. La technique utilise également une table de hachage (par thread) pour éviter les récursions dans la vérification à l’exécution. Les expressions utilisant des quantificateurs sont considérées comme non exécutables par la technique, et aucun code Java n’est généré pour ces expressions.
Korat a proposé une technique pour générer à la fois des cas de test et des oracles à partir de spécifications JML . La technique de Korat génère des cas de test à partir des préconditions et des invariants et des oracles à partir des postconditions et des invariants. Araujo et al. ont étendu JML en ajoutant des contrats concurrents et ont proposé un support d’exécution pour permettre la vérification à l’exécution des assertions qui spécifient des propriétés concurrentes .
Peters et Parnas ont introduit une approche pour générer des oracles de test à partir de la documentation formelle . La documentation est donnée sous une forme tabulaire qui consiste en des relations qui spécifient les interfaces des procédures et est traduite en oracles en code C et C++. L’élément central de la documentation formelle consiste en des expressions de prédicats écrites dans une variante de la logique des prédicats avec des constructions spéciales pour traiter les fonctions partielles. Similaire à d’autres techniques d’oracle basées sur la spécification, cette technique traite les quantificateurs en les restreignant à des ensembles finis.
Pour permettre des itérations sur des ensembles d’éléments avec des quantificateurs, Peters et Parnas introduisent des prédicats définis inductivement. Pour un ensemble S (à utiliser dans les quantifications), un prédicat défini inductivement P est défini avec trois éléments I, G et Q. L’ensemble initial I contient un nombre fini d’éléments, G est une fonction, appelée » fonction génératrice « , qui génère les éléments de l’ensemble, et Q est un prédicat qui caractérise les propriétés de l’ensemble. L’ensemble S est défini comme le moindre ensemble construit dans les étapes inductives ci-dessous :
S0 = I
Sn + 1 = Sn ∪ {G(x)|x ∈ Sn ∧ Q(x)}
I, G et Q doivent être définis pour satisfaire une condition spéciale qui assure que l’ensemble construit S est fini .
Peters et Parnas proposent une approche pour traduire les documentations tabulaires en code C . Comme la forme des expressions utilisées dans les documentations est bien définie, la traduction se fait systématiquement.
D’autres spécifications basées sur l’état sont également utilisées pour dériver des oracles de test. Les modèles UML sont généralement informels ; néanmoins, Bouquet et al. ont défini un sous-ensemble de UML 2.1, nommé UML-MBT, qui est suffisamment précis pour générer automatiquement des cas de test. UML-MBT comprend des diagrammes de classes, des machines à états et un sous-ensemble d’OCL 2.0. Bouquet et al. utilisent des spécifications écrites en VDM-SL pour générer des oracles de test.