UP | HOME

Vers la programmation certifiée sans bug

Table of Contents

1 La chasse aux bugs

Avec l'utilisation massive de l'informatique à toute échelle, les défaillances logicielles ont des conséquences majeures. Certaines sont directement visibles : les atteintes à la sécurité, les défaillances catastrophiques de systèmes critiques, les dysfonctionnements en tous genres. D'autres sont moins visibles, comme la chasse systématique aux bugs, organisée par les développeurs de logiciels.

Cette chasse est coûteuse :

  • les développeurs peuvent passer cinquante pour cent de leur temps de programmation à trouver et à réparer des bugs,
  • un tiers environ des dépenses concerne l'assurance de la qualité logicielle.

(Les sources ne sont pas mentionnées, du fait qu'elles sont de seconde main. Ces chiffres, incertains donc, donnent un ordre de grandeur. Données bienvenues !)

Il a souvent été observé que le coût d'un bug augmente en fonction du temps de découverte : plus il est découvert tôt, mieux c'est. Par exemple, un moyen courant de détecter un bug consiste à tester. Le test arrive après l'implémentation. Un moyen courant d'éviter des bugs est de recourir au typage statique. Le typage s'applique pendant l'implémentation, au moment du codage. La plupart du temps, le typage ne coûte rien et permet d'éviter tout test dédié aux erreurs de typage.

L'objectif du cours est de systématiser l'approche du typage en chassant si bien les bugs statiquement qu'ils disparaissent complètement. Cette chasse systématique s'appuie sur la logique.

2 La logique - Science et pratique de l'inférence

Étymologie de logique : du grec λογική / logikê, terme dérivé de λόγος / lógos, raison, langage, raisonnement

But : inférer des propositions à partir d'autres propositions, en utilisant des règles

  • Science et pratique

Deux théories pour l'inférence

  • théorie de la démonstration ("proof theory")
  • théorie des modèles ("model theory")

Théorie de la démonstration

  • Depuis Gentzen (1934) : deux systèmes d'inférence, la déduction naturelle et le calcul des séquents
    • ensembles de règles et d'axiomes permettant de valider des jugements logiques (des déductions entre des hypothèses et des conclusions)

Théorie des modèles

  • Depuis Tarski (1933, modernisé en 1956) : le concept de vérité dans les langages formalisés
    • une relation de vérification entre une interprétation (attribuant une valeur aux constantes non logiques), une valuation (attribuant une valeur à chaque variable libre) et une formule logique

Exemple : le calcul propositionnel - Voir le cours.

Méta-théorie

  • Adéquation : si une proposition est prouvable, alors elle est vérifiée dans toute interprétation.
  • Complétude (réciproque) : si une proposition est vérifiée dans toute interprétation, alors elle est prouvable.
  • Incomplétude d'une théorie (un ensemble d'axiomes) : il existe une proposition qui n'est pas prouvable ni réfutable (dont la négation n'est pas prouvable) dans cette théorie.
  • Décidabilité : une théorie est décidable s'il existe un algorithme qui détermine si une proposition est prouvable ou non dans cette théorie.

3 L'informatique - Science et pratique de la transformation de l'information

But : transformer de l'information en utilisant des machines programmées à l'aide de langages pour implémenter des algorithmes (extrait d'un programme scolaire)

  • Science et pratique

Théorie et pratique très diversifiées

  • Syntaxe et sémantique des langages de programmation
    • Syntaxe : notation pour les programmes
    • Sémantique : dénotation pour les programmes
  • Grands paradigmes de la programmation
    • Programmation impérative
    • Programmation objet
    • Programmation fonctionnelle
    • Programmation logique
  • Algorithmique
    • Description de méthodes de calcul dans des pseudo-langages
  • Machines
    • De l'architecture matérielle à la spécification abstraite de machines

4 Relation entre logique et informatique

Relation ?

  • inférer = transformer ?
  • proposition = information ?
  • systèmes d'inférence = machines programmées à l'aide de langages pour implémenter des algorithmes ?

Relation de la logique (mathématique) et de l'informatique à double sens

  • interprétation informatique de sujets et d'objets logiques (décidabilité de logiques, recherche automatisée de preuves)
  • interprétation logique de sujets et d'objets informatiques (vérification de programmes, logique de programmes)

Exemples

  • On the Unusual Effectiveness of Logic in Computer Science, de Joseph Y. Halpern, Robert Harper, Neil Immerman, Moshe Y. Vardi, Phokion G. Kolaitis, Victor Vianu (1999)
    • Connexion entre la logique descriptive et la complexité calculatoire
    • Représentation logique des langages de requêtes des bases de données
    • Influence de la théorie des types sur la programmation
    • Raisonnement sur le partage de connaissances avec la logique épistémique (et sa modalité "X sait que")
    • Connexion entre la logique et la vérification automatique de systèmes à état

5 Programmation fonctionnelle, programmation logique

Correspondance fondamentale (dite de Curry-Howard)

  • proposition = type
  • preuve = programme

Langage de programmation fonctionnelle

  • syntaxe pour les propositions et pour les preuves
  • programmation := détermination d'une preuve de la proposition (la spécification)
  • sémantique statique : typage
  • sémantique dynamique : simplification de la preuve

Langage de programmation logique

  • syntaxe pour les propositions
  • programmation := détermination d'une proposition
  • sémantique statique : bonne formation syntaxique
  • sémantique dynamique : recherche de la preuve en utilisant des tactiques propres au langage

Historiquement,

  • utilisation de logiques élémentaires pour la programmation fonctionnelle,
  • utilisation de logiques plus riches pour la programmation logique.

Aujourd'hui

  • logique très riche pour la programmation fonctionnelle,
  • logiques très riches pour la programmation en logique.

6 L'assistant à la démonstration Coq

Outil logiciel interactif permettant

  • de programmer dans un langage fonctionnel très riche,
  • de programmer en logique,
  • de raisonner dans une logique très riche,
  • de définir des tactiques automatisant la recherche de preuves dans une logique très riche.

7 Objectifs du cours

  • Comprendre les fondations logiques de la programmation
  • Utiliser l'assistant à la démonstration Coq pour certifier des programmes en utilisant les fondations logiques

8 Évaluation

  • Exercices en continu - en binôme
  • Examen final sur machine - individuel

Author: Hervé Grall
Version history: v1: 2020-01-06.
Comments or questions: Send a mail.
The webpage content is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.