,
44 tweets,
4 min read
Read on Twitter
Bonjour! Ce matin nous reprenons notre programme sur la preuve de programmes.
L'algorithme, c'est l'idée un peu "dans l'abstrait" d'un processu de calcul. Le programme, c'est ce qui fonctionnera en vrai.
Le programme est écrit dans un langage de programmation. Il en existe PLEIN, et ceux existant depuis longtemps ont évolué.
Premier choix: va-t-on prouver des propriétés sur l'algorithme (en évacuant plein de détails) ou sur le programme ?
Surtout que dans un programme, il n'y a pas que des algorithmes, il y a beaucoup de "plomberie" qui peut aussi avoir des bugs.
Dans un logiciel grand public, la partie algorithmiquement intéressante est souvent petite, le reste c'est de la plomberie et du câblage.
Bref il est souvent plus simple de tester/prouver un algorithme, mais souvent ce qu'on veut vraiment tester/prouver c'est le programme.
Et donc le programme est écrit dans un langage de programmation. Et celui-ci n'a pas forcément un sens bien défini !
Le langage de programmation a une documentation ou suit un standard écrit en langue naturelle (généralement anglais).
Cette documentation peut être imprécise, sujette à interprétation.
Dans le cas de fonctionnalités euh délicates de certains langages, on se demande même si le standard a un sens.
(@spun_off en parlera mieux que moi mais les histoires de types effectifs et de type aliasing dans le standard du langage C...)
(Nous pouvons également évoquer les modèles mémoires concurrents du langage C++, qui ont euh suscité le débat.)
On entend vraiment dans les colloques "le comité de standardisation pense maintenant que ce qu'il a écrit n'a guère de sens".
Vous me direz que la loi civile est aussi souvent mal écrite et sans sens bien défini. Mais on ne fait pas de preuve mathématique dessus!
Mais revenons en donc à notre programme écrit dans son langage de programmation. Il ne s'exécute pas directement sur la machine.
En effet, le programme est fait pour être lu et écrit par des humains, en reflétant (plus ou moins) leur idées "de haut niveau".
La machine, elle, ne sait faire que des choses assez élémentaires (lire, écrire une donnée, faire +, -, *...) mais très vite.
Il faut donc traduire ce que l'humain a écrit en ce que la machine sait faire: c'est ce que l'on appelle la COMPILATION.
(Oui je sais il existe aussi des interpréteurs etc. mais ne compliquons pas.)
La compilation, c'est une forme de TRADUCTION (coucou @languesdefeu): on préserve le sens entre deux langages différents.
Souvent le langage d'arrivée est le langage du processeur dans la machine. Vous savez, le truc fait par Intel ou AMD.
La documentation de l'architecture Intel fait 4744 pages. Oui, ça enfonce le code du travail. software.intel.com/sites/default/…
Ok, toute cette documentation n'est pas pertinente pour l'écriture de compilateurs. Mais tout de même...
Le compilateur peut tenter une traduction "mot à mot" (en vrai c'est plus compliqué), relativement simple.
C'est d'ailleurs ce que certains industriels font en avionique critique: comme ça ils peuvent comparer facilement original et traduction.
vocabulaire: original="code source" traduction="code objet"
Toutefois, cette traduction planplan produit du code objet inefficace: lent. Peut être 2 fois, 5 fois plus lent qu'une meilleure traduction.
Rappelez vous ce que je disais sur les modèles climatiques: plus on calcule vite, plus on est précis, plus vite on peut se mettre à jour...
Dans un téléphone portable, on visera un code objet consommant moins d'énergie...
Donc on va faire de la compilation OPTIMISANTE, qui cherche à diminuer le coût (temps) du code objet en préservant le sens du source.
Le compilateur optimisant réorganise le code pour qu'il fasse la même chose mais plus efficacement.
Vous vous doutez bien qu'un compilateur optimisant est plus compliqué qu'un non optimisant. Donc peut contenir plus de bugs.
Un bug de compilation, dans le meilleur des cas, c'est le compilateur qui "plante" et dit "erreur interne, bye bye".
Dans le pire des cas, le compilateur, silencieusement, produit du code objet incorrect.
Mieux encore, du code objet incorrect qui marche dans une partie des cas mais plante ou donne de faux résultats dans d'autres cas.
Pour se prémunir des problèmes d'interprétation des standards de langages et des bug de compilation, on peut prouver sur le code objet.
C'est cependant pénible: dans le code objet tout est décomposé en petites opérations, on a perdu la vision de haut niveau.
Le code source, c'est "la voiture a 4 portes et un capot", le code objet c'est la description de chacune des petites pièces.
Où donc placer la preuve? Sur les algorithmes ou protocoles idéalisés? Sur le code source? Sur le code objet?
(Ce n'est pas une question rhétorique, hier encore je discutais de ce problème avec @camille_coti )
Si je prouve sur un programme, comment sais-je que j'ai la même définition du sens du langage que celle du compilateur ?
Ne pourrait-on pas prouver que le compilateur compile correctement ?
Je tenterai d'aborder ces questions aujourd'hui !
