Yannick Moy de AdaCore présente à travers une démo de GNAT Studio comment SPARK va aider à détecter les erreurs. Il nous montre comment en progressant dans la définition des pre-conditions, post-conditions et assertions il est possible d'arriver à une preuve du programme avec SPARK.

Associations

Abonnez-vous

Tags