Simulateur de feux où les états dangereux sont interdits par le typage.
TerminéSprint S9+S35 · 8 points
En bref, sans jargonpour les non-informaticiensLire le résuméRefermer
Ce que c'est
Un carrefour à feux tricolores, qu'on fait fonctionner sur la page, dont le programme rend un accident impossible : deux voies ne peuvent jamais être au vert en même temps.
À quoi ça sert
C'est la méthode des logiciels où une erreur coûte cher : aéronautique, ferroviaire, médical.
Ce que ça montre
La programmation sûre, et la preuve mathématique qu'un programme ne peut pas se tromper, en langage Ada.
Le programme Ada a calculé tous les états que peut prendre son contrôleur, et ce qu'y change une seconde ou une demande de passage. Cette page ne fait que suivre ces transitions : demandez le passage sur un axe et regardez le vert de l'autre se raccourcir, jamais sous 10 secondes, sans jamais deux axes ouverts en même temps.
Chronogramme des 60 dernières secondes
Vert de 30 s au nord-sud et 20 s à l'est-ouest, orange de 3 s, rouge intégral de 2 s, comme la simulation du programme. Le typage, les contrats et la preuve SPARK garantissent le reste (voir le README).
Technologies
Ada
SPARK
GNAT
AUnit
Alire
Qui fait quoi
Ada
Le contrôleur de feux : les phases forment un type énuméré, si bien qu'un état « deux axes au vert » ne peut pas s'écrire ; le programme exporte aussi l'automate que rejoue la fiche.
SPARK
Prouve l'absence d'erreur à l'exécution, les contrats, et qu'au moins un axe est toujours au rouge.
GNAT
Le compilateur Ada, avertissements traités en erreurs, sur Linux, Windows et macOS.
AUnit
Les tests : cycle complet, demandes de passage, durées hors bornes refusées, automate de la fiche sûr.
Alire
Installe la même chaîne GNAT et les dépendances (AUnit, gnatprove), en local comme en CI.