Abonnez-vous à Universalis pour 1 euro

PROGRAMMATION

Méthodes formelles

Les méthodes formelles sont des techniques informatiques d'une grande rigueur permettant, à l'aide de langages spécialisés et de règles logiques, de s'assurer (idéalement) de l'absence de tout défaut de programmes informatiques – ce qui est crucial en particulier lorsque ceux-ci mettent en jeu des vies humaines –, de logiciels ou de démonstrations mathématiques.

Besoins et enjeux

En quelques décennies, la miniaturisation des processeurs a permis leur introduction dans des équipements de toutes tailles et dédiés à toutes sortes de tâches, qu'il s'agisse d'électroménager, de centrales nucléaires, d'appareils médicaux, de cartes à puce, d'automates bancaires, de systèmes de télécommunications, d'automobiles ou d'avions de ligne. Tous ces équipements sont donc pilotés ou contrôlés par des programmes logiciels, et cela change complètement la donne quant aux dispositions à prendre pour éviter les défaillances. Pour mettre au point la partie analogique de ces systèmes, les moyens mathématiques à mettre en œuvre relèvent de l'analyse, plus précisément du calcul différentiel. Sommairement, on a affaire à des fonctions continues, produisant en sortie des effets voisins lorsque les déviations en entrée sont petites. Les systèmes discrets, et tout particulièrement les programmes, sont en revanche fondamentalement instables. Au niveau des portes logiques ou des instructions machine, le moindre changement de bit a potentiellement des effets arbitrairement grands. Dans un programme exprimé dans un langage de haut niveau, une modification minime dans une valeur, une expression ou une instruction conduit tout aussi facilement à d'énormes différences de comportement. Observons en passant l'importance de cette caractéristique du logiciel, sa flexibilité : par comparaison avec un système matériel, il est très facile d'intervenir sur un programme pour le corriger, en changer les fonctionnalités, mais aussi d'y introduire des erreurs (y compris en voulant le corriger).

Abstraitement, l'exécution d'un programme reste un enchaînement de décisions distinctes. L'enchaînement précis qui se déroule dépend de conditions initiales variables (exemple : paramètres fournis lors d'un appel, ou lecture d'informations captées dans l'environnement). L'enjeu est alors de s'assurer que l'on aura les effets souhaités – ce qui soulève la question de spécifier les comportements désirables (ou indésirables) ; nous y reviendrons plus bas –, et ce dans tous les cas. Ce dernier point fait écho à ce qui précède : alors que, pour les systèmes analogiques, nos mathématiques portent d'emblée sur des plages entières de valeurs, la complexité spécifique du logiciel (et des systèmes matériels basés sur des circuits logiques) provient de la nécessité intrinsèque d'étudier exhaustivement, et souvent un par un, une multitude de cas de figure (sans perte de généralité, on ne s'attarde pas ici sur le cas intermédiaire des programmes numériques). Le travail qui en résulte est principalement un travail de raisonnement logique. La difficulté vient de ce que le nombre de cas à considérer tend à s'élever très vite avec l'augmentation de la complexité des systèmes, des fonctions à réaliser, de la multiplication des combinaisons, etc.

En pratique, ceux qui sont chargés de concevoir et de réaliser un système programmé raisonnent constamment : par cas sur les valeurs traitées, par récurrence sur le nombre de tours de boucle effectués, etc. En règle générale, il s'agit d'un mélange de bon sens, de réutilisation de résultats antérieurs et d'expérimentation. Mais ces raisonnements sont rarement explicites, sinon ils présenteraient les deux défauts rédhibitoires d'être beaucoup trop longs et beaucoup trop fastidieux. Ils[...]

La suite de cet article est accessible aux abonnés

  • Des contenus variés, complets et fiables
  • Accessible sur tous les écrans
  • Pas de publicité

Découvrez nos offres

Déjà abonné ? Se connecter

Écrit par

  • : professeur des Universités, professeur à l'université de Grenoble-I-Joseph-Fourier

Classification

Autres références

  • ALGORITHME

    • Écrit par et
    • 5 919 mots
    • 4 médias
    ...langage utilisé et de la représentation des données. Ainsi, il est possible d’écrire un programme calculant les éléments de la suite de Fibonacci dans deux langages de programmation différents, comme Python et C, tout en considérant qu’ils sont des réalisations, ou mieux, des implantations du même algorithme....
  • BREVET DU PREMIER ROBOT INDUSTRIEL

    • Écrit par
    • 290 mots

    Un inventeur indépendant, George C. De Vol, développe et brevette aux États-Unis, en 1954, un système d'enregistrement magnétique capable de commander les opérations d'une machine. Pour le vendre, il crée, avec l'ingénieur Joseph F. Engelberger, la première entreprise de robotique, Unimation Inc....

  • COBOL (common business oriented language)

    • Écrit par
    • 332 mots

    Langage de programmation de haut niveau spécialement conçu pour des applications commerciales et des applications de gestion. Cobol autorise le traitement des gros fichiers sur supports séquentiels ou sélectifs à l'aide d'un vocabulaire et d'une syntaxe censés rappeler l'anglais courant....

  • FORTRAN (FORmula TRANslation)

    • Écrit par
    • 314 mots

    Historiquement, Fortran peut être décrit comme l'un des premiers langages de programmation de haut niveau ayant permis d'écrire de manière complète et détaillée des procédures de calcul ou des algorithmes complexes sans faire appel au langage d'assemblage. Sa syntaxe proche de celle du langage...

  • Afficher les 16 références