C'est dur, mais ca marche. En gros le principe est le suivant : tu spécifies tes opérations avec un langage formel (posé avec des définitions j'espère que tu est pas allergique aux maths) avec les pré et post conditions, invariants et compagnie.
En suite il y a des analyseurs qui te transforment ta spec en langage informatique - les transformations sont elles-même prouvées - , tu compile et tu a les parties de ton programme que tu voulais prouver.
Le hic, c'est qu'il faudrait que le compilateur et le système sur lequel ca tourne soient aussi prouvé, mais bon c'est déjà mieux qu'un truc écrit directement.
C'est pas fun, c'est pas facile, et en plus c'est pas optimisé du tout. Mais c'est la seule manière de faire du code prouvé.
En passant, n'oublie pas que les processeurs aussi ne sont pas complètement testés, et que l'on ne sait pas si 1 612 313 *3461 donne le bon résultat.
(en tout cas 1+1 chez moi ca marche)
# Ca existe (enfin presque).
Posté par Anonyme . En réponse au journal couverture de code. Évalué à 5.
http://www.cours.polymtl.ca/log2000/Intro_Z.pdf(...) http://www.ingenieurs-supelec.org/groupespro/automobile/MethodeB/sl(...) )
C'est dur, mais ca marche. En gros le principe est le suivant : tu spécifies tes opérations avec un langage formel (posé avec des définitions j'espère que tu est pas allergique aux maths) avec les pré et post conditions, invariants et compagnie.
En suite il y a des analyseurs qui te transforment ta spec en langage informatique - les transformations sont elles-même prouvées - , tu compile et tu a les parties de ton programme que tu voulais prouver.
Le hic, c'est qu'il faudrait que le compilateur et le système sur lequel ca tourne soient aussi prouvé, mais bon c'est déjà mieux qu'un truc écrit directement.
C'est pas fun, c'est pas facile, et en plus c'est pas optimisé du tout. Mais c'est la seule manière de faire du code prouvé.
En passant, n'oublie pas que les processeurs aussi ne sont pas complètement testés, et que l'on ne sait pas si 1 612 313 *3461 donne le bon résultat.
(en tout cas 1+1 chez moi ca marche)