L'objectif des méthodes formelles est d'assurer la qualité des logiciels en proposant une méthode alternative aux méthodes de test traditionnelle. Cette méthode repose principalement sur un traitement symbolique des programmes et de propriétés logiques qui expriment ce que l'on attend de ces programmes: les spécifications. Plusieurs méthodes utilisent ce principe et nous verrons quelques exemples introductifs
L'objectif de ce cours n'est pas de rendre les étudiants experts dans ce domaine, mais de les familiariser avec une technique d'assurance qualité qu'il seront peut-être amenés à proposer dans leur milieu professionnel.
La logique de Hoare est utilisée pour construire de façon sûre des programmes dans des langages impératifs (les langages traditionnels, avec affectation de variable, conditionnelle, boucle). Elle permet d'associer des annotations aux instructions d'un programme. Ces annotations sont des formules logiques qui expriment les propriétés attendues des variables du programme au point où l'annotation est insérée. Un calcul symbolique permet d'assurer que l'ensemble des annotations portées par un programme est cohérent avec ce programme. Si la réponse est positive, on est alors certain que le programme effectue les calculs spécifiés par les annotations. Ce programme est alors sans erreurs!
La logique de Hoare ne résout pas absolument tous les problèmes, principalement parce que la vérification de cohérence engendre des conditions logico-mathématiques qu'il faut vérifier, et cette vérification est indécidable: il n'existe donc pas de méthode complètement automatique pour assurer qu'un programme satisfait un spécification. Néanmoins, cette méthode apporte amélioration notable à la qualité des programmes.
De nombreuses méthodes formelles reposent sur la manipulation de formule logiques. Pour certains problèmes, ces formules logiques peuvent être réduite à des valeurs de vérité pour un certain nombre (souvent très grand) de variables. Il s'agit alors de vérifier qu'une formule booléenne contenant des milliers de variables est bien toujours vraie, pour toutes les valeurs possibles de ces variables. Nous allons étudier deux techniques de raisonnement automatique sur ces formules: un algorithme de satisfiabilité et une bibliothèque de traitement de diagrammes de décision binaire.
Pour certains systèmes informatiques, la description du comportement attendu nécessite d'exprimer des propriétés dans lesquelles le temps apparait: tel programme répond toujours, telle erreur n'arrive jamais, telle réponse arrive immédiatement. Pour traiter ce genre de spécifications, les chercheurs ont proposé de fournir un traitement particulier pour des formules logiques dans lesquelles les mots-clefs "toujours", "immédiatement", "jamais", et les autres sont considérés comme des connecteurs au même titre que "et", "ou", "non". La recherche de validité de ces formules logiques fait appel à des calculs automatiques sur les formules logiques, que nous étudierons.