L’adamantium est un métal imaginé par Marvel Comics et décrit comme étant le plus résistant de tous les métaux…

Et si on mettait de « l’Ada-mantium » dans nos applications ?!

L’Ada-mantium est un alliage de sept préconisations sur la mise en œuvre du langage Ada ou sa technologie afférente.

La première des préconisations concerne la technologie GNAT et l’option --gnatVa. Cette option permet d’activer des vérifications de validité supplémentaires et non requises au niveau de la run-time. Cette option n’est pas active par défaut du fait de son impact sur la charge processeur. Il est préférable d’associer cette option au pragma de configuration GNAT Initialize_Scalars (qui est sémantiquement proche du pragma normalisé Normalize_Scalars). Ce ‘duo’ option/pragma permet de traquer très efficacement des variables non initialisées.

La deuxième préconisation concerne toujours la technologie GNAT et son modèle d’élaboration statique qui est celui par défaut. En effet, ce dernier doit être privilégié car en plus du fait qu’il garantisse de ne pas avoir la levée de l’exception Program_Error (access before elaboration), il permet de mettre clairement en exergue des problèmes de structuration/architecture du code.

La troisième préconisation consiste à tirer un maximum parti des warnings émis par le compilateur, aussi bien au niveau de son front-end que de son back-end. Pour rappel, il n’est pas raisonnable de livrer un code avec des warnings. Concernant les warnings volontairement désactivés, ils ne doivent l’être que sous le couvert d’une justification.

La quatrième préconisation consiste à prendre au moins en compte les exigences listées dans l’annexe H du manuel de référence Ada. Cette annexe, dédiée aux High Integrity Systems, liste ces dernières dans le but de faciliter le développement d’applications critiques du point de vue de la sécurité ou de la sûreté.

Plus précisément, ces exigences permettent :

De maîtriser temporellement et spatialement l’exécution d’un programme.
De restreindre l’utilisation de certains traits du langage.

Ainsi donc, l’annexe ARM §H.4 (High Integrity Restrictions) propose, sous la forme de pragma Restrictions (voir ARM §13.12), une façon simple de produire ce type d’applications en fonction par exemple des contraintes associées à la run-time utilisée. Dans le cadre de la mise en œuvre du tasking Ada, des restrictions dédiées peuvent aussi être appliquées (voir ARM §D.7).

L’implémentation peut proposer des restrictions qui lui sont propres. Le code ci-dessous présente un exemple de restrictions standards et spécifiques à l’implémentation GNAT.

-- ARM §H.4:
pragma Restrictions (No_Allocators, No_Exceptions, No_Recursion, No_Unchecked_Access);

-- GNAT RM §5:
pragma Restrictions (No_Enumeration_Maps, No_Secondary_Stack);

Il est à rappeler que les profils d’exécution Ravenscar et Jorvik (voir ARM §D.13) s’appuient principalement sur un ensemble de restrictions. Ces profils ont, entre autres, pour objet de policer les applications multitâches en vue, par exemple, d’une certification.

La cinquième préconisation consiste à faire en sorte qu’une partie significative de votre code soit Stone Level au sens SPARK du terme.

Pour rappel, SPARK propose 5 niveaux d’adoption :

Stone Level : Le code respecte le subset-Ada/SPARK : on s’affranchit d’erreurs de base tout en respectant un standard.
Bronze Level : Le flot de données est vérifié : plus de variables non initialisées, plus de problèmes d’aliasing, plus d’affectations inutiles, plus de variables non utilisées.
Silver Level : Absence d’exceptions run-time (AoRTE).
Gold Level : Respect des propriétés du programme : respect des contrats sur les opérations et les types.
Platinum Level : Preuve complète des exigences du logiciel.

Ici, Stone Level doit être vu comme un standard de codage vous permettant d’avoir un code de bonne facture en évitant par exemple les effets de bord dans les expressions ou en limitant l’utilisation des pointeurs. Le fait d’être Stone Level vous permettra aussi d’accéder simplement au Bronze Level sans avoir obligatoirement une connaissance approfondie de SPARK.

La sixième préconisation concerne l’adoption du paradigme de la programmation par contrat.

Depuis Ada₂₀₁₂, on peut décrire formellement et nativement les propriétés d’une opération en y associant une sémantique via les Pré/Post-conditions, les invariants et les prédicats. Il est ainsi possible de décrire ce que le programme doit faire et le langage garantit que ce que vous avez dit sera fait. Il y a ainsi une garantie sur le respect du contrat. Cette vérification peut être faite soit par la run-time ou prouvée formellement au travers de SPARK.

La mise en œuvre de la programmation par contrat est aussi la clé pour accéder aux niveaux Silver Level, Gold Level et Platinum Level de SPARK.

La septième et dernière préconisation est : « Rendez les choses aussi simples que possible, mais pas plus simples » (Albert Einstein).

Voilà ! Vous avez maintenant la recette pour concocter de l’Ada-mantium. Vos applications Ada vont ainsi devenir plus robustes, mais pas indestructibles !

Références¶

[1] : GNAT User’s Guide for Native Platforms

[2] : GNAT Reference Manual

[3] : SPARK User’s Guide

[4] : Ada Reference Manual

[5] : Ada Reference Manual — 2022 edition