Tu pourrais nous expliquer le genre de code qui est fournis à un assistant de preuve, par exemple, en utilisant du pseudo code ?
Dans le milieu de l'aéronautique, il est souvent question de comparaison de modèles et de confrontation d'interprétation de spec entre 2 équipes utilisant des outils différents. Donc, on a une équipe qui développe le programme et l'autre un modèle sous une autre forme. On compare ensuite les résultats de tests définit par avance par l'équipe de test (mais qui pourrait être généré automatiquement par classe d'équivalence des entrées et couverture de code)
Le but serait ici de facilité la vie de la deuxième équipe.
[^] # Re: prouveur automatique/assistant de preuve
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.
Dans le milieu de l'aéronautique, il est souvent question de comparaison de modèles et de confrontation d'interprétation de spec entre 2 équipes utilisant des outils différents. Donc, on a une équipe qui développe le programme et l'autre un modèle sous une autre forme. On compare ensuite les résultats de tests définit par avance par l'équipe de test (mais qui pourrait être généré automatiquement par classe d'équivalence des entrées et couverture de code)
Le but serait ici de facilité la vie de la deuxième équipe.
"La première sécurité est la liberté"