Spark est un sous-ensemble d'Ada et se compile donc normalement avec le compilateur Ada
Un code Spark peut (et devrait sinon, autant faire de l'Ada, c'est plus simple) être vérifié
Les temps de compilation sont donc les temps du compilateur Ada qui n'est pas non plus franchement le plus rapide du Far West.
Ceci dit, c'est normal, il compile beaucoup plus de choses qu'un compilateur C, ne serait-ce que les spécifications (en gros, les headers C) et vérifie tout une batterie de règles de cohérence (compatibilité des types, portée des pointeurs...).
A cela, s'ajoute dans le cas de Spark, l'étape de preuve du programme.
Cette étape fait appel à un autre outil que le compilateur dont le but est de transcrire les éléments Spark (post-, pré-conditions, invariants de boucle, assertions) dans le langage Why3.
Le "programme" Why3 est ensuite envoyé au moteur de preuve pour être analysé. Cette étape peut être très longue, beaucoup plus qu'une simple compilation mais l'enjeu n'est vraiment pas le même qu'une "simple" compilation.
A ce jour, les "provers" CVC4, Z3 et Alt-Ergo sont supportés et il est parfois nécessaire de faire passer son programme à la moulinette d'un ou plusieurs de ces programmes.
Petit anecdote, après discussion avec Yannick Moy à l'OSXP , Adacore a commencé à décorer la bibliothèque standard avec du Spark, histoire de prouver qu'il n'y a pas d'erreur dedans... Il semblerait qu'ils aient d'ailleurs trouvé une petite erreur passée inaperçue depuis des lustres :D
Voilà, j'espère avoir répondu à la question sans avoir dit trop de conneries :D
[^] # Re: Perf
Posté par Blackknight (site web personnel, Mastodon) . En réponse au journal la rouille et la comtesse. Évalué à 7. Dernière modification le 20 novembre 2021 à 11:03.
Il faut distinguer deux choses:
Les temps de compilation sont donc les temps du compilateur Ada qui n'est pas non plus franchement le plus rapide du Far West.
Ceci dit, c'est normal, il compile beaucoup plus de choses qu'un compilateur C, ne serait-ce que les spécifications (en gros, les headers C) et vérifie tout une batterie de règles de cohérence (compatibilité des types, portée des pointeurs...).
A cela, s'ajoute dans le cas de Spark, l'étape de preuve du programme.
Cette étape fait appel à un autre outil que le compilateur dont le but est de transcrire les éléments Spark (post-, pré-conditions, invariants de boucle, assertions) dans le langage Why3.
Le "programme" Why3 est ensuite envoyé au moteur de preuve pour être analysé. Cette étape peut être très longue, beaucoup plus qu'une simple compilation mais l'enjeu n'est vraiment pas le même qu'une "simple" compilation.
A ce jour, les "provers" CVC4, Z3 et Alt-Ergo sont supportés et il est parfois nécessaire de faire passer son programme à la moulinette d'un ou plusieurs de ces programmes.
Petit anecdote, après discussion avec Yannick Moy à l'OSXP , Adacore a commencé à décorer la bibliothèque standard avec du Spark, histoire de prouver qu'il n'y a pas d'erreur dedans... Il semblerait qu'ils aient d'ailleurs trouvé une petite erreur passée inaperçue depuis des lustres :D
Voilà, j'espère avoir répondu à la question sans avoir dit trop de conneries :D