Ça m'a rappelé avec émotion les pré et post conditions. La belle époque.
Et encore, si les pré et post conditions permettant de générer des assertions automatiques en Ada, elles ne sont qu'un bout de ce que l'on peut utiliser en Spark.
Il y a notamment toute une série d'aspects (c'est comme ça qu'on dit) spécifiques à Spark permettant entre autre de décrire les dépendances aux variables globales, à la description d'un état au sein d'un package...
C'est complexe et long mais super intéressant :)
En cadeau, quelques liens :
- Le user guide
- Une introduction à Spark
- Un guide pour passer son code Ada vers du code Spark. Attention, toutes les constructions Ada ne sont pas autorisées en Spark, ce dernier ne travaille que sur un subset sans ambiguïté pour un "prouveur"
[^] # Re: Ada aujourd'hui ?
Posté par Blackknight (site web personnel, Mastodon) . En réponse à la dépêche Alire, le package manager d'Ada. Évalué à 5. Dernière modification le 05 juin 2022 à 23:59.
Et encore, si les pré et post conditions permettant de générer des assertions automatiques en Ada, elles ne sont qu'un bout de ce que l'on peut utiliser en Spark.
Il y a notamment toute une série d'aspects (c'est comme ça qu'on dit) spécifiques à Spark permettant entre autre de décrire les dépendances aux variables globales, à la description d'un état au sein d'un package...
C'est complexe et long mais super intéressant :)
En cadeau, quelques liens :
- Le user guide
- Une introduction à Spark
- Un guide pour passer son code Ada vers du code Spark. Attention, toutes les constructions Ada ne sont pas autorisées en Spark, ce dernier ne travaille que sur un subset sans ambiguïté pour un "prouveur"
Bonne lecture