Gérard Berry Algorithmes, machines et langages Collège de France LEÇON DE CLÔTURE Où va l'informatique ? 26 février 2019

Gérard Berry Algorithmes, machines et langages Collège de France LEÇON DE CLÔTURE Où va l'informatique ? 26 février 2019

Gérard Berry Algorithmes, machines et langages Collège de France LEÇON DE CLÔTURE Où va l'informatique ? 26 février 2019

Gérard Berry Algorithmes, machines et langages Année 2014-2015 Prouver les programmes : pourquoi, quand, comment ? Sixième leçon : Vérification et optimisation booléennes d'automates et circuits Ce dernier cours de 2014-2015 introduit les méthodes implicites de manipulation de systèmes de transitions, à travers les méthodes de calcul booléen utilisées à la fois pour la vérification formelles et pour l’optimisation de circuits électroniques et de programmes qui peuvent se réduire au calcul booléen. Ces méthodes ont révolutionné le domaine en permettant des vérifications formelles de systèmes dont le calcul explicite des états et transitions est impossible, car la taille des formules manipulées par les méthodes implicites est largement indépendante de celle des systèmes qu’ils décrivent. Nous expliquons d’abord les codages booléens d’ensembles, de relations et de fonctions, et montrons comment calculer l’image directe et l’image inverse de sous-ensembles par des fonctions. Nous étudions ensuite les codages booléens d’automates déterministes et non-déterministes, ainsi que leurs implémentations en circuits électroniques. Nous rappelons le fait que le circuit canoniquement associé à un automate non-déterministe est lui déterministe comme tous les circuits combinatoirement acycliques, ce qui montre clairement que le qualificatif « non-déterminisme » est particulièrement mal choisi : en vérification booléenne comme en optimisation de circuits, il est inutile de déterminiser les automates, et c’est souvent nuisible à cause de l’explosion exponentielle que la déterminisation peut produire. Nous montrons comment la vérification formelle de propriétés de sûreté définies par des observateurs se réduit au calcul des états accessibles, et comment effectuer ce calcul de manière implicite. Nous introduisons la première structure fondamentale du calcul booléen, les Binary Decision Diagrams, développés par R. Bryant au milieu des années 1980 (et indépendamment par J-P. Billion chez Bull en France), et expliquons pourquoi ils permettent de faire les calculs nécessaires au passage à la grande échelle; nous mentionnons leurs limitations, qui sont inévitables car le calcul booléen est NP-complet. Les BDDs seront étudiés beaucoup plus en profondeur dans le cours 2015-2015. Pour terminer, nous montrons que le codage booléen permet de réaliser des optimisations très efficaces des circuits engendrés par les programmes Esterel. Nous insistons sur le fait que la structure du langage source et la façon d’y programmer les applications sont essentiels pour la qualité de l’optimisation finale : c’est grâce à l’interaction de la séquence, du parallélisme et de la préemption hiérarchique des comportements que les circuits engendrés par Esterel sont systématiquement meilleurs que ceux programmés et optimisés par les méthodes classiques, au moins en ce qui concerne leurs parties contrôle.

Gérard Berry Algorithmes, machines et langages Année 2014-2015 Prouver les programmes : pourquoi, quand, comment ? Sixième leçon : Vérification et optimisation booléennes d'automates et circuits Ce dernier cours de 2014-2015 introduit les méthodes implicites de manipulation de systèmes de transitions, à travers les méthodes de calcul booléen utilisées à la fois pour la vérification formelles et pour l’optimisation de circuits électroniques et de programmes qui peuvent se réduire au calcul booléen. Ces méthodes ont révolutionné le domaine en permettant des vérifications formelles de systèmes dont le calcul explicite des états et transitions est impossible, car la taille des formules manipulées par les méthodes implicites est largement indépendante de celle des systèmes qu’ils décrivent. Nous expliquons d’abord les codages booléens d’ensembles, de relations et de fonctions, et montrons comment calculer l’image directe et l’image inverse de sous-ensembles par des fonctions. Nous étudions ensuite les codages booléens d’automates déterministes et non-déterministes, ainsi que leurs implémentations en circuits électroniques. Nous rappelons le fait que le circuit canoniquement associé à un automate non-déterministe est lui déterministe comme tous les circuits combinatoirement acycliques, ce qui montre clairement que le qualificatif « non-déterminisme » est particulièrement mal choisi : en vérification booléenne comme en optimisation de circuits, il est inutile de déterminiser les automates, et c’est souvent nuisible à cause de l’explosion exponentielle que la déterminisation peut produire. Nous montrons comment la vérification formelle de propriétés de sûreté définies par des observateurs se réduit au calcul des états accessibles, et comment effectuer ce calcul de manière implicite. Nous introduisons la première structure fondamentale du calcul booléen, les Binary Decision Diagrams, développés par R. Bryant au milieu des années 1980 (et indépendamment par J-P. Billion chez Bull en France), et expliquons pourquoi ils permettent de faire les calculs nécessaires au passage à la grande échelle; nous mentionnons leurs limitations, qui sont inévitables car le calcul booléen est NP-complet. Les BDDs seront étudiés beaucoup plus en profondeur dans le cours 2015-2015. Pour terminer, nous montrons que le codage booléen permet de réaliser des optimisations très efficaces des circuits engendrés par les programmes Esterel. Nous insistons sur le fait que la structure du langage source et la façon d’y programmer les applications sont essentiels pour la qualité de l’optimisation finale : c’est grâce à l’interaction de la séquence, du parallélisme et de la préemption hiérarchique des comportements que les circuits engendrés par Esterel sont systématiquement meilleurs que ceux programmés et optimisés par les méthodes classiques, au moins en ce qui concerne leurs parties contrôle.

Gérard Berry Algorithmes, machines et langages Année 2014-2015 Prouver les programmes : pourquoi, quand, comment ? Sixième leçon : La vérification de modèles (model-checking) Ce cours termine la présentation générale des méthodes de vérification formelle par la vérification de modèles, plus connue sous son nom anglais original de model-checking. Cette méthode est bien différente des précédentes car elle s’intéresse essentiellement aux programmes d’états finis, ceux dont on peut au moins conceptuellement dérouler complètement toutes les exécutions possibles en temps et espace fini. De plus, contrairement aux méthodes précédemment décrites, le model-checking s’intéresse principalement aux programmes parallèles. Le parallélisme peut y être synchrone comme dans les circuits ou les langages synchrones présentés les années précédentes, ou asynchrones comme dans les protocoles de communication, les réseaux et les algorithmes distribués. Le model-checking est né au début des années 1980, quasi-simultanément en deux endroits : Grenoble avec J-P. Queille et J. Sifakis, qui ont développé le système CESAR et sa logique temporelle, et les USA avec E. Clarke et E. Emerson qui ont développé la logique temporelle CTL et le système EMV. Ces travaux ont donné le prix Turing 2007 à Clarke, Emerson et Sifakis. Ils s’appuyaient eux-mêmes sur les travaux d’Amir Pnueli (prix Turing en 1996) sur la logique temporelle. Le model-checking s’est considérablement développé ensuite, et constitue certainement la méthode formelle la plus utilisée dans l’industrie, en particulier dans la CAO de circuits. L’idée de base est de construire le graphe de toutes les exécutions possibles d’un programme, qu’on appelle son modèle. Ce modèle peut prendre la forme d’une structure de Kripke (logicien et philosophe de la logique modale), c’est-à-dire d’un graphe où les états sont étiquetés par des prédicats élémentaires, ou encore d’une structure de transitions, où les étiquettes sont portées par les transitions entre états. Une fois construit, le modèle devient indépendant du langage qui l’a engendré. Pour raisonner sur un modèle, un moyen très répandu est l’utilisation de logiques temporelles, définissent les propriétés temporelles à l’aide de propriétés élémentaires des états ou transitions et de quantificateurs sur les états ou les chemins de son graphe. On peut ainsi exprimer et vérifier des propriétés de sûreté (absence de bugs), comme « à aucun moment l’ascenseur ne peut voyager la porte ouverte », d’absence de blocages de l’exécution, ou de vivacité, comme « l’ascenseur finira par répondre à toutes les demandes des passagers » ou encore « chaque processus obtiendra infiniment souvent la ressource partagée s’il la demande infiniment souvent ». Nous présenterons d’abord la logique CTL*, la plus générale, qui permet d’imbriquer arbitrairement les quantifications d’états et de chemin sur les structures de Kripke. Mais cette logique très expressive est difficile à utiliser et les calculs y sont d’un coût prohibitif. Deux sous-logiques différentes sont utilisées : LTL (Linear Temporal Logic), qui ne quantifie pas sur les états et considère donc seulement des traces linéaires, et CTL, logique arborescente qui permet de quantifier sur les chemins mais avec des restrictions par rapport à CTL*. Ces deux logiques sont d’expressivités différentes et ont chacune des avantages et des inconvénients que nous discuterons brièvement. LTL est la logique la mieux adaptées pour la vérification de propriétés de vivacité, comme le montre L. Lamport (prix Turing 2014) avec son système TLA+. Mais, au contraire, elle ne permet pas d’exprimer des prédicats sur l’existence de calculs particuliers. La modélisation par systèmes de transitions, systématisée par R. Milner (prix Turing 1992) dans l’étude des calculs de processus communicants, permet de bien mieux composer les exécutions de ces processus parallèles. Une notion fondamentale introduite par Milner est la bisimulation, équivalence comportementale qui permet de comparer finement ce que peuvent faire ou ne pas faire les processus. Nous montrons que la réduction par bisimulation fournit une alternative très intéressante et intuitive aux logiques temporelles pour la vérification de modèles, en particulier en liaison avec les langages synchrones. Une dernière façon de conduite la vérification de modèles est de remplacer les formules temporelles par des programmes observateurs, qui prennent en entrée les entrées et les sorties du programme à vérifier et ont pour charge d’envoyer un signal de bug s’ils détectent une anomalie. Cette méthode est en particulier idéale pour les langages synchrones comme Esterel et Lustre étudiés les années précédentes, car les observateurs peuvent être écrits dans ces mêmes langages de façon plus simple qu’en logique temporelle, au moins pour les propriétés de sûreté qui sont les plus importantes dans leur domaine d’application. Cette méthode n’est en fait pas disjointe des précédentes, cat les formules temporelles sont souvent traduites en automates observateurs pour la vérification. Il faut noter que, dans tous les cas, le programme à vérifier évolue dans un environnement qu’il est important et souvent indispensable de modéliser aussi avec les mêmes techniques. La modélisation de l’environnement n’est pas forcément plus simple que celle du programme lui-même, et, particulièrement en logique temporelle, il faut s’assurer que le modèle d’environnement construit n’est pas vide, sous peine que toutes les propriétés à vérifier ne deviennent trivialement vraies. Cela demande d’étudier la satisfiabilité des formules d’environnement, ce qui n’est pas forcément simple. Nous terminons le cours par une brève présentation de l’algorithmique du model-checking, qui se divise en deux grandes classes de méthodes et de systèmes associés. Les méthodes explicites énumèrent systématiquement les états et transitions possibles. Comme la taille du modèle peut être gigantesque, ces méthodes utilisent des machines massivement parallèles ainsi que de nombreuses façons de réduire la complexité de l’analyse : calcul à la volée du modèle et des propriétés, exploration aléatoire du graphe, réduction par utilisation par symétrie ou commutation d’actions indépendantes, abstractions diverses, etc. Les méthodes implicites, introduites plus tard, utilisent des représentations symboliques des espaces d’états et de transitions, par exemple en utilisant des fonctions caractéristiques d’ensembles. Leur avantage est que la taille des formules servant à l’exploration du modèle n’est plus associée à la taille de l’espace d’états, leurs inconvénients étant que leur temps de calcul est difficilement prévisible et leur implémentation sur machine parallèle problématique. Les Binary Decision Diagrams (BDDs), la plus ancienne des représentations implicites en calcul booléen, seront étudiés au cours suivant. La satisfaction Booléenne (SAT) ou modulo théories (SMT) devient de plus en plus la méthode de choix pour le model-checking implicite. Nous l’illustrerons sur l’exemple bien connu du Sudoku, pertinent ici même si sa résolution n’est pas vraiment du model-checking temporel. Comme les méthodes explicites, les méthodes implicites font appel à de nombreuses techniques pour lutter contre l’explosion exponentielle du temps de calcul ou de la taille mémoire. Elles seront étudiées les années suivantes. Nous insisterons enfin sur deux propriétés essentielles des model-checkers, qui les rendent attirants pour les utilisateurs : le fait qu’ils ne demandent pas à leur utilisateur de connaître précisément les techniques qu’ils emploient, et leur faculté de produire des contre-exemples minimaux pour les propriétés fausses, qui est primordiale à la fois pour le débogage et la génération de tests.

Gérard Berry Algorithmes, machines et langages Année 2014-2015 Prouver les programmes : pourquoi, quand, comment ? Cinquième leçon : La vérification de modèles (model-checking) Ce cours termine la présentation générale des méthodes de vérification formelle par la vérification de modèles, plus connue sous son nom anglais original de model-checking. Cette méthode est bien différente des précédentes car elle s’intéresse essentiellement aux programmes d’états finis, ceux dont on peut au moins conceptuellement dérouler complètement toutes les exécutions possibles en temps et espace fini. De plus, contrairement aux méthodes précédemment décrites, le model-checking s’intéresse principalement aux programmes parallèles. Le parallélisme peut y être synchrone comme dans les circuits ou les langages synchrones présentés les années précédentes, ou asynchrones comme dans les protocoles de communication, les réseaux et les algorithmes distribués. Le model-checking est né au début des années 1980, quasi-simultanément en deux endroits : Grenoble avec J-P. Queille et J. Sifakis, qui ont développé le système CESAR et sa logique temporelle, et les USA avec E. Clarke et E. Emerson qui ont développé la logique temporelle CTL et le système EMV. Ces travaux ont donné le prix Turing 2007 à Clarke, Emerson et Sifakis. Ils s’appuyaient eux-mêmes sur les travaux d’Amir Pnueli (prix Turing en 1996) sur la logique temporelle. Le model-checking s’est considérablement développé ensuite, et constitue certainement la méthode formelle la plus utilisée dans l’industrie, en particulier dans la CAO de circuits. L’idée de base est de construire le graphe de toutes les exécutions possibles d’un programme, qu’on appelle son modèle. Ce modèle peut prendre la forme d’une structure de Kripke (logicien et philosophe de la logique modale), c’est-à-dire d’un graphe où les états sont étiquetés par des prédicats élémentaires, ou encore d’une structure de transitions, où les étiquettes sont portées par les transitions entre états. Une fois construit, le modèle devient indépendant du langage qui l’a engendré. Pour raisonner sur un modèle, un moyen très répandu est l’utilisation de logiques temporelles, définissent les propriétés temporelles à l’aide de propriétés élémentaires des états ou transitions et de quantificateurs sur les états ou les chemins de son graphe. On peut ainsi exprimer et vérifier des propriétés de sûreté (absence de bugs), comme « à aucun moment l’ascenseur ne peut voyager la porte ouverte », d’absence de blocages de l’exécution, ou de vivacité, comme « l’ascenseur finira par répondre à toutes les demandes des passagers » ou encore « chaque processus obtiendra infiniment souvent la ressource partagée s’il la demande infiniment souvent ». Nous présenterons d’abord la logique CTL*, la plus générale, qui permet d’imbriquer arbitrairement les quantifications d’états et de chemin sur les structures de Kripke. Mais cette logique très expressive est difficile à utiliser et les calculs y sont d’un coût prohibitif. Deux sous-logiques différentes sont utilisées : LTL (Linear Temporal Logic), qui ne quantifie pas sur les états et considère donc seulement des traces linéaires, et CTL, logique arborescente qui permet de quantifier sur les chemins mais avec des restrictions par rapport à CTL*. Ces deux logiques sont d’expressivités différentes et ont chacune des avantages et des inconvénients que nous discuterons brièvement. LTL est la logique la mieux adaptées pour la vérification de propriétés de vivacité, comme le montre L. Lamport (prix Turing 2014) avec son système TLA+. Mais, au contraire, elle ne permet pas d’exprimer des prédicats sur l’existence de calculs particuliers. La modélisation par systèmes de transitions, systématisée par R. Milner (prix Turing 1992) dans l’étude des calculs de processus communicants, permet de bien mieux composer les exécutions de ces processus parallèles. Une notion fondamentale introduite par Milner est la bisimulation, équivalence comportementale qui permet de comparer finement ce que peuvent faire ou ne pas faire les processus. Nous montrons que la réduction par bisimulation fournit une alternative très intéressante et intuitive aux logiques temporelles pour la vérification de modèles, en particulier en liaison avec les langages synchrones. Une dernière façon de conduite la vérification de modèles est de remplacer les formules temporelles par des programmes observateurs, qui prennent en entrée les entrées et les sorties du programme à vérifier et ont pour charge d’envoyer un signal de bug s’ils détectent une anomalie. Cette méthode est en particulier idéale pour les langages synchrones comme Esterel et Lustre étudiés les années précédentes, car les observateurs peuvent être écrits dans ces mêmes langages de façon plus simple qu’en logique temporelle, au moins pour les propriétés de sûreté qui sont les plus importantes dans leur domaine d’application. Cette méthode n’est en fait pas disjointe des précédentes, cat les formules temporelles sont souvent traduites en automates observateurs pour la vérification. Il faut noter que, dans tous les cas, le programme à vérifier évolue dans un environnement qu’il est important et souvent indispensable de modéliser aussi avec les mêmes techniques. La modélisation de l’environnement n’est pas forcément plus simple que celle du programme lui-même, et, particulièrement en logique temporelle, il faut s’assurer que le modèle d’environnement construit n’est pas vide, sous peine que toutes les propriétés à vérifier ne deviennent trivialement vraies. Cela demande d’étudier la satisfiabilité des formules d’environnement, ce qui n’est pas forcément simple. Nous terminons le cours par une brève présentation de l’algorithmique du model-checking, qui se divise en deux grandes classes de méthodes et de systèmes associés. Les méthodes explicites énumèrent systématiquement les états et transitions possibles. Comme la taille du modèle peut être gigantesque, ces méthodes utilisent des machines massivement parallèles ainsi que de nombreuses façons de réduire la complexité de l’analyse : calcul à la volée du modèle et des propriétés, exploration aléatoire du graphe, réduction par utilisation par symétrie ou commutation d’actions indépendantes, abstractions diverses, etc. Les méthodes implicites, introduites plus tard, utilisent des représentations symboliques des espaces d’états et de transitions, par exemple en utilisant des fonctions caractéristiques d’ensembles. Leur avantage est que la taille des formules servant à l’exploration du modèle n’est plus associée à la taille de l’espace d’états, leurs inconvénients étant que leur temps de calcul est difficilement prévisible et leur implémentation sur machine parallèle problématique. Les Binary Decision Diagrams (BDDs), la plus ancienne des représentations implicites en calcul booléen, seront étudiés au cours suivant. La satisfaction Booléenne (SAT) ou modulo théories (SMT) devient de plus en plus la méthode de choix pour le model-checking implicite. Nous l’illustrerons sur l’exemple bien connu du Sudoku, pertinent ici même si sa résolution n’est pas vraiment du model-checking temporel. Comme les méthodes explicites, les méthodes implicites font appel à de nombreuses techniques pour lutter contre l’explosion exponentielle du temps de calcul ou de la taille mémoire. Elles seront étudiées les années suivantes. Nous insisterons enfin sur deux propriétés essentielles des model-checkers, qui les rendent attirants pour les utilisateurs : le fait qu’ils ne demandent pas à leur utilisateur de connaître précisément les techniques qu’ils emploient, et leur faculté de produire des contre-exemples minimaux pour les propriétés fausses, qui est primordiale à la fois pour le débogage et la génération de tests.

Gérard Berry Algorithmes, machines et langages Année 2014-2015 Prouver les programmes : pourquoi, quand, comment ? Quatrième leçon : Des logiques d'ordre supérieur à la programmation vérifiée en Coq Ce cours complète le précédent en terminant la présentation des méthodes générales de preuve de programmes par celle fondée sur les logiques d’ordre supérieur (celles où l’on peut aussi quantifier sur les prédicats) et sur le lambda-calcul déjà présenté en détail dans le cours 2009-2010. Nous montrons d’abord pourquoi l’ordre supérieur est plus expressif que l’ordre un. Par exemple, pour prouver une propriété par récurrence, il faut avoir en calcul des prédicats un schéma d’axiome de récurrence qui engendre un axiome particulier par prédicat à étudier, et donc une infinité d’axiomes ; en ordre supérieur, un seul axiome standard suffit puisqu’on peut quantifier universellement le prédicat de travail. D’autres avantages apparaîtront dans la suite du cours. Un inconvénient est bien sûr une plus grande complexité de la logique et de certains des algorithmes permettant de la traiter. Nous décrirons d’abord brièvement les systèmes HOL de M. Gordon, HOL-Light de J. Harrison, PVS de N. Shankar, S. Owre et J. Rushby, et Isabelle de L. Paulson, ce dernier étant en fait un méta-système logique dans lequel plusieurs logiques peuvent être définies. Ces systèmes ont conduit à des preuves très importantes en pratique : la preuve de correction de l’arithmétique entière et flottante du Pentium d’Intel par J. Harrison après le fameux bug de division du Pentium Pro qui a coûté 470 millions de dollars à Intel en 1994 ; la preuve de correction du micronoyau de système d’exploitation seL4 effectuée par G. Klein et. al. à NICTA Sydney en utilisant Isabelle (cf. le séminaire de D. Bolignano le 11 mars 2015 pour une autre preuve de système d’exploitation). Nous présentons ensuite avec plus de détails le système Coq, développé en France et titulaire de grandes récompenses récentes. Coq est fondé sur le calcul des constructions CoC de G. Huet et T. Coquand (1984) et sa version inductive CiC développée par C. Paulin, qui parlera en séminaire, à la suite de ce cours. Coq diffère des systèmes classiques par le fait qu’il intègre complètement calcul et preuve dans un formalisme très riche, incorporant et développant considérablement des idées et théorèmes de de Bruijn (Automath, 1967), Girard (SystemF, 1972), etc. Gallina, le langage de programmation de Coq est un langage typé d’ordre supérieur, c’est-à-dire dont les types peuvent eux-mêmes être des fonctions. Le typage est décidable, et le système de types garantit que tous les calculs de termes bien typés se terminent sur des formes normales uniques. La programmation classique est facilitée par la couche inductive, qui permet des définitions récursives puissantes mais à terminaison garantie. Grâce à la mise en pratique de la correspondance fondamentale de Curry-Howard entre calculs et preuves, il n’y a plus vraiment de différence entre calculer et prouver. Ainsi, un programme a pour type sa spécification alors qu’une preuve a pour type le théorème qu’elle démontre, ce de façon absolument identique. De plus, les preuves sont des fonctions standards du calcul, au même titre que les fonctions sur les types de données classiques. Enfin, une fois un programme développé et prouvé en Coq, on peut en extraire automatiquement un code objet directement exécutable écrit en Caml, correct par construction et normalement efficace. Tout cela donne à Coq une richesse considérable à la fois pour spécifier, programmer, prouver et exporter, quatre activités qui deviennent complètement intégrées. Le cours se terminera par la présentation de deux succès majeurs de Coq : d’abord le compilateur certifié CompCert de X. Leroy, seul compilateur C ayant passé le filtre des tests aléatoires présenté dans le cours du 4 mars ; ensuite la preuve complètement formelle de grands théorèmes mathématiques par G. Gonthier et. al., avec en particulier le fameux théorème de Feit-Thompson dont la preuve classique fait pas moins de 250 pages de lourdes mathématiques.

Gérard Berry Algorithmes, machines et langages Année 2014-2015 Prouver les programmes : pourquoi, quand, comment ? Quatrième leçon : Des logiques d'ordre supérieur à la programmation vérifiée en Coq Ce cours complète le précédent en terminant la présentation des méthodes générales de preuve de programmes par celle fondée sur les logiques d’ordre supérieur (celles où l’on peut aussi quantifier sur les prédicats) et sur le lambda-calcul déjà présenté en détail dans le cours 2009-2010. Nous montrons d’abord pourquoi l’ordre supérieur est plus expressif que l’ordre un. Par exemple, pour prouver une propriété par récurrence, il faut avoir en calcul des prédicats un schéma d’axiome de récurrence qui engendre un axiome particulier par prédicat à étudier, et donc une infinité d’axiomes ; en ordre supérieur, un seul axiome standard suffit puisqu’on peut quantifier universellement le prédicat de travail. D’autres avantages apparaîtront dans la suite du cours. Un inconvénient est bien sûr une plus grande complexité de la logique et de certains des algorithmes permettant de la traiter. Nous décrirons d’abord brièvement les systèmes HOL de M. Gordon, HOL-Light de J. Harrison, PVS de N. Shankar, S. Owre et J. Rushby, et Isabelle de L. Paulson, ce dernier étant en fait un méta-système logique dans lequel plusieurs logiques peuvent être définies. Ces systèmes ont conduit à des preuves très importantes en pratique : la preuve de correction de l’arithmétique entière et flottante du Pentium d’Intel par J. Harrison après le fameux bug de division du Pentium Pro qui a coûté 470 millions de dollars à Intel en 1994 ; la preuve de correction du micronoyau de système d’exploitation seL4 effectuée par G. Klein et. al. à NICTA Sydney en utilisant Isabelle (cf. le séminaire de D. Bolignano le 11 mars 2015 pour une autre preuve de système d’exploitation). Nous présentons ensuite avec plus de détails le système Coq, développé en France et titulaire de grandes récompenses récentes. Coq est fondé sur le calcul des constructions CoC de G. Huet et T. Coquand (1984) et sa version inductive CiC développée par C. Paulin, qui parlera en séminaire, à la suite de ce cours. Coq diffère des systèmes classiques par le fait qu’il intègre complètement calcul et preuve dans un formalisme très riche, incorporant et développant considérablement des idées et théorèmes de de Bruijn (Automath, 1967), Girard (SystemF, 1972), etc. Gallina, le langage de programmation de Coq est un langage typé d’ordre supérieur, c’est-à-dire dont les types peuvent eux-mêmes être des fonctions. Le typage est décidable, et le système de types garantit que tous les calculs de termes bien typés se terminent sur des formes normales uniques. La programmation classique est facilitée par la couche inductive, qui permet des définitions récursives puissantes mais à terminaison garantie. Grâce à la mise en pratique de la correspondance fondamentale de Curry-Howard entre calculs et preuves, il n’y a plus vraiment de différence entre calculer et prouver. Ainsi, un programme a pour type sa spécification alors qu’une preuve a pour type le théorème qu’elle démontre, ce de façon absolument identique. De plus, les preuves sont des fonctions standards du calcul, au même titre que les fonctions sur les types de données classiques. Enfin, une fois un programme développé et prouvé en Coq, on peut en extraire automatiquement un code objet directement exécutable écrit en Caml, correct par construction et normalement efficace. Tout cela donne à Coq une richesse considérable à la fois pour spécifier, programmer, prouver et exporter, quatre activités qui deviennent complètement intégrées. Le cours se terminera par la présentation de deux succès majeurs de Coq : d’abord le compilateur certifié CompCert de X. Leroy, seul compilateur C ayant passé le filtre des tests aléatoires présenté dans le cours du 4 mars ; ensuite la preuve complètement formelle de grands théorèmes mathématiques par G. Gonthier et. al., avec en particulier le fameux théorème de Feit-Thompson dont la preuve classique fait pas moins de 250 pages de lourdes mathématiques.

Gérard Berry Algorithmes, machines et langages Année 2014-2015 Prouver les programmes : pourquoi, quand, comment ? Troisième leçon : Les méthodes générales : assertions, réécriture, interprétation abstraite, logiques et assistants de preuve Il y a deux principaux types de méthodes formelles pour la preuve de programme : les méthodes générales, qui s’adressent à tous les types de programmes et seront présentées dans ce cours, et celles de la vérification de modèles (model-checking), qui s’intéressent principalement aux programmes à espaces d’états finis et aux circuits électroniques et seront traitées dans le cours no 5 du 25 mars 2015. La nécessité de traiter les programmes comme des objets mathématiques à part entière a été reconnue par A. Turing dès 1949. Il a alors introduit la notion d’assertion associant un prédicat logique à un point de contrôle du programme, ainsi que l’importance de la notion d’ordre bien fondé pour montrer la terminaison des programmes. Son approche par assertions est la première que nous traiterons dans le cours. Elle a été étendue et perfectionnée par R. Floyd, C.A.R. Hoare, E.W. Dijkstra, et bien d’autres, pour aboutir à une théorie et une pratique complètes de la définition logique des langages de programmation et de la vérification de programmes, applicables initialement aux programmes séquentiels impératifs. La notion d’assertion a été ensuite étendue en celle de contrat (assume/guarantee) à respecter par les fonctions ou modules d’un programme, applicable aussi aux langages objets et aux langages parallèles. En 1963, dans un article fondateur militant pour le traitement mathématique de la programmation et introduisant une brochette remarquable de nouveaux concepts, J. McCarthy a introduit l’idée bien différente d’utiliser la réécriture de termes comme outil applicable à la fois pour l’optimisation de programmes et leur vérification formelle. Cette approche, la seconde que nous étudierons, a eu une longue descendance dans les systèmes de vérification (Boyer&More, ACL2, PVS, Key, ProVerif, etc.), et continue d'irriguer les autres approches. Elle a eu des succès remarquables en circuits, en avionique, en sécurité, etc. La troisième approche historique est celle de la sémantique dénotationnelle des langages introduite par Scott et Strachey vers 1970. Ici, un programme est interprété comme une fonction dans un espace topologique ordonné par un ordre d’information, et toutes les fonctions sont rendues totales par l’ajout explicite d’éléments indéfinis. Une théorie générale du point fixe dans les espaces ordonnés permet d’interpréter de façon uniforme les boucles, la récursion et la programmation fonctionnelle d’ordre supérieur. Au début des années 1970, cette théorie a été à l’origine du pionnier des assistants de preuve de programmes, LCF, créé par Milner et al. Mais le traitement explicite de l’indéfini s’est révélé trop compliqué, et les assistants de preuve ont ensuite suivi un autre chemin. La sémantique dénotationnelle a cependant eu un succès considérable dans une autre approche de la vérification, l’interprétation abstraite créé par P. et R. Cousot en 1977. L’idée est ici de travailler avec des assertions portant non plus sur les valeurs exactes calculées, mais sur une abstraction de celles-ci, comme la preuve par 9 le fait pour détecter des erreurs dans la multiplication. De nombreux domaines abstraits ont été développés, ainsi que des méthodes algorithmiques générales de combinaison de ces domaines et d’accélération des calculs de points fixes. L’interprétation abstraite est maintenant développée industriellement. Elle a permis de vérifier des propriétés critiques de très gros programmes, comme l’absence d’erreurs à l’exécution dans le code de pilotage de l’Airbus A380. Elle est également utilisée pour l’évaluation du temps de calcul maximal de logiciels embarqués et pour accélérer les calculs dans d’autres types de système de vérification. La quatrième approche traitée dans ce cours est la vérification par assistants de preuves logiques. L’idée est ici de traduire le problème de vérification informatique en un problème purement logique, et de fournir une aide à la vérification à travers un système de tactiques et d’interaction homme-machine permettant d’organiser les preuves logiques à grand échelle, augmenté d’automatisations partielles pour des sous-domaines spécifiques utilisant par exemple des techniques de réécriture. Les assistants actuels traitent plusieurs types de logique, allant du calcul des prédicats de premier ordre augmenté par la théorie des ensembles (Rodin pour Event B, etc.) ou par la logique temporelle (TLA+), jusqu’aux calculs d’ordre supérieur (HOL, Isabelle, Coq, etc.). Ce cours présentera sommairement les ateliers de premier ordre, les ordres supérieurs étant traités dans le cours suivant. Nous prendrons l’exemple des formalismes B et Event-B de J.-R. Abrial (orateur du dernier séminaire du 1er avril 2015). L’atelier B a été utilisé pour la spécification, la programmation et la vérification formelle de logiciels critiques pour la conduite du RER A, de la ligne 14 (Meteor) du métro parisien, et de plusieurs autres systèmes ferroviaires. Event-B et son système Rodin sont une évolution de B vers les systèmes événementiels qui sont ubiquitaires dans l’informatique embarquée.