SPARK (langage de programmation)

Considérez la spécification du sous-programme Ada ci-dessous :

procédure Incrémenter (X : entrée sortie Type_Compteur);

En Ada pur, cela pourrait incrémenter la variable Xde un ou de mille ; ou cela pourrait définir un compteur global Xet renvoyer la valeur originale du compteurX ; ou cela pourrait ne rien faire avec X.

Avec SPARK 2014, des contrats sont ajoutés au code pour fournir davantage d'informations sur le fonctionnement d'un sous-programme. Par exemple, la spécification ci-dessus peut être modifiée comme suit :

procédure Incrémenter (X : entrée sortie Type_Compteur)  avec Global => null , Dépend => (X => X);

Cela précise que la Incrementprocédure n'utilise aucune variable globale (ni mise à jour ni lecture) et que le seul élément de données utilisé pour calculer la nouvelle valeur de Xest Xseul.

La spécification peut également être rédigée comme suit :

procédure Incrémenter (X : type_compteur d'entrée/sortie )  avec Global => (Entrée/Sortie => Compteur), Dépend => (Nombre => (Nombre, X), X => null);

Ceci spécifie que Incrementla variable globale sera utilisée Countdans le même package que Increment, que la valeur exportée de Countdépend des valeurs importées de Countet X, et que la valeur exportée de Xne dépend d'aucune variable et sera dérivée uniquement de données constantes.

Si GNATprove est ensuite exécuté sur la spécification et le corps correspondant d'un sous-programme, il analysera ce dernier afin de construire un modèle du flux d'informations. Ce modèle sera ensuite comparé aux annotations et toute divergence sera signalée à l'utilisateur.

Ces spécifications peuvent être étendues en précisant diverses propriétés qui doivent être vérifiées lors de l'appel d'un sous-programme ( préconditions ) ou qui le seront une fois l'exécution du sous-programme terminée ( postconditions ). Par exemple :

procédure Incrémentation (X : entrée sortie Type_Compteur)  avec Global => null, Dépend => (X => X), Pré => X < Counter_Type'Dernier, Post => X = X'Ancien + 1;

Ceci précise non seulement que Xest dérivé de lui-même, mais aussi qu'avant Incrementl'appel, Xdoit être strictement inférieur à la dernière valeur possible de son type (pour garantir que le résultat ne déborde jamais ) et qu'après, Xsera égal à la valeur initiale Xplus un.

GNATprove peut également générer un ensemble de conditions de vérification (CV). Celles-ci servent à déterminer si certaines propriétés sont vérifiées pour un sous-programme donné. Au minimum, GNATprove génère des CV pour s'assurer qu'aucune erreur d'exécution ne peut se produire au sein d'un sous-programme, par exemple :

• Indice de tableau hors limites
• violation de plage de type
• division par zéro
• débordement numérique

Si une postcondition ou toute autre assertion est ajoutée à un sous-programme, GNATprove générera également des VC qui exigent que l'utilisateur démontre que ces propriétés sont vérifiées pour tous les chemins possibles à travers le sous-programme.

En interne, GNATprove utilise le langage intermédiaire Why3 et le générateur de VC , ainsi que les démonstrateurs de théorèmes CVC4 , Z3 et Alt-Ergo pour résoudre les VC. L'utilisation d'autres démonstrateurs (y compris des vérificateurs de preuves interactifs) est également possible grâce à d'autres composants de la suite d'outils Why3.

Les origines de cette technologie remontent à 1987, avec des travaux menés à l' Université de Southampton . La première version de SPARK (basée sur Ada 83) a été développée au sein de cette université, avec le soutien du ministère britannique de la Défense , par Bernard Carré et Trevor Jennings. Le nom SPARK est dérivé de SPADE Ada Kernel , en référence au sous-ensemble SPADE du langage de programmation Pascal .

Par la suite, le langage a été progressivement étendu et perfectionné, d'abord par Program Validation Limited, puis par Praxis Critical Systems Limited. En 2004, Praxis Critical Systems Limited est devenue Praxis High Integrity Systems Limited, et les travaux sur SPARK se sont poursuivis. En janvier 2010, la société est devenue Altran Praxis .

Début 2009, Praxis a formé un partenariat avec AdaCore et a publié SPARK Pro sous les termes de la licence GPL. Cette publication a été suivie en juin 2009 par la sortie de SPARK GPL Edition 2009, destinée aux communautés du logiciel libre et open source (FOSS) et du monde universitaire.

En janvier 2013, Altran-Praxis a changé de nom pour devenir Altran, qui est devenu Capgemini Engineering en avril 2021 (suite à la fusion d'Altran avec Capgemini ).

La première version Pro de SPARK 2014 a été annoncée le 30 avril 2014 et a été rapidement suivie par l'édition GPL de SPARK 2014, destinée aux communautés FLOSS et académiques.

SPARK a été utilisé dans de nombreuses applications industrielles concrètes. Son intégration le plus tôt possible dans le processus de conception est généralement considérée comme donnant les résultats les plus favorables.