LDRA Testbed est capable de vérifier que les assertions sont conformes pendant la durée d'exécution. Cela nécessite de comparer les valeurs de variables à une condition booléenne spécifique. Les assertions sont écrites sous forme de commentaires spéciaux dans le code source, dans le même style que de nombreuses notations de spécification formelles.
LDRA Testbed scanne un fichier source afin de trouver d'éventuelles chaînes spécifiques. La chaîne exacte et certaines des règles de correspondance sont décrites dans un fichier de paramètre. Chaque assertion doit commencer et finir par l'une de ces chaînes spéciales. Chaque ligne d'une assertion (y compris les chaînes spéciales de début et de fin) doit faire partie d'un commentaire normal dans le langage source. Cela signifie que si la source d'origine a été soumise au compilateur, elle sera compilée comme étant normale avec les assertions traitées en tant que commentaires. Lorsque que le début d'une chaîne d'assertion est détecté, les lignes suivantes (jusqu'au commentaire de fin spécial) sont traitées en tant qu'expression d'assertion. L'expression est analysée afin de vérifier qu'il s'agit bien d'une expression booléenne valide. La syntaxe explicite peut être personnalisée, la forme standard correspondant à celle des langages tels qu'Ada, C et Pascal.
Après l'analyse de conformité dynamique, l'assertion (ci-dessus) est développée, comme indiqué ci-dessous:
Une instrumentation est ajoutée avant et après l'expression afin de détecter sa valeur de vérité. L'instrumentation s'effectue de manière à ce qu'une assertion erronée entraîne un processus de "défaillance" qui transmet un numéro de référence signalant cette assertion spécifique. Les assertions proviennent généralement d'exigences et de documents de spécification. Elles peuvent servir à spécifier des postulats d'entrée ou de sortie s'appliquant à une section de code. LDRA Testbed génère une source instrumentée (avec assertions activées) et un processus de gestion de "défaillance" que l'on peut personnaliser. Les schémas [à droite] démontrent l'effet du code source une fois que l'analyse sémantique exacte a transformé les assertions.
L'analyse sémantique exacte est une combinaison de méthodes formelles et de tests pragmatiques qui vérifie la conformité des assertions pendant la durée d'exécution.
Résumé de l'analyse sémantique exacte
- Effectue une analyse sémantique exacte du code de source
- Produit un diagnostic pour le code source
- Spécifie les postulats d'entrée et de sortie s'appliquant à une section du code source
- Vérifie que les entrées correspondent aux champs prédéterminés
- Vérifie que les indices de boucle et de tableau correspondent aux limites fixées
Obtenir plus d'informations
Pour plus d'informations sur cette fonctionnalité spécifique de TBsafe et sa disponibilité, veuillez remplir le formulaire de réponse de LDRA ou envoyer un e-mail à .
|
