C'est pas une question de trivialité, c'est une question de grammaire.
Ce qu'à fait X. Leroy, c'est de prouver le parser, la transformation du code source en code intermédiaire , l'allocation de registres et la traduction du code intermédiaire en code objet.
Prouver du code C, c'est plutôt l'oeuvre de Jean-Christophe Filliatre http://why.lri.fr
C'est vrai, que vu la taille de la grammaire, prouver du C non trivial est pas chose facile.
« Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker
[^] # Re: Esperons que la qualité suivra
Posté par Ontologia (site web personnel) . En réponse à la dépêche Sortie de la version 4.1 du compilateur GCC. Évalué à 3.
Ce qu'à fait X. Leroy, c'est de prouver le parser, la transformation du code source en code intermédiaire , l'allocation de registres et la traduction du code intermédiaire en code objet.
Prouver du code C, c'est plutôt l'oeuvre de Jean-Christophe Filliatre http://why.lri.fr
C'est vrai, que vu la taille de la grammaire, prouver du C non trivial est pas chose facile.
« Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker