Méthode formelle (informatique)

En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement, à l'aide de logique mathématique, sur un programme informatique ou du matériel électronique numérique, afin de démontrer leur validité par rapport à une certaine spécification. Elles reposent sur les sémantiques des programmes, c'est-à-dire sur des descriptions mathématiques formelles du sens d'un programme donné par son code source (ou, parfois, son code objet). Ces méthodes permettent d'obtenir une très forte assurance de l'absence de bug dans les logiciels (Evaluation Assurance Level, Safety Integrity Level). Elles sont utilisées dans le développement des logiciels les plus critiques. Leur amélioration et l'élargissement de leurs champs d'application pratique sont la motivation de nombreuses recherches scientifiques en informatique. Comment vérifier que l'identité est correcte ? Une vérification naïve pourrait consister à examiner toutes les valeurs possibles de , à les croiser avec toutes les valeurs possibles de et, pour chaque couple, à calculer , puis et à s'assurer que l'on obtient le même résultat. Si les domaines de et de sont grands, cette vérification peut être très longue. Et si les domaines sont infinis (par exemple les réels), cette vérification ne peut pas être exhaustive. En vérification formelle, on utilise des valeurs symboliques et on applique les règles qui régissent le et l'. Ici, les règles pourraient être: En se servant de ces règles, on arrive à montrer que . La vérification comprend plusieurs approches, souvent complémentaires : la démonstration de théorèmes est une approche qui tend à être automatisée et assistée par ordinateur. Elle consiste à énoncer des propositions et à les démontrer dans un système de déduction de la logique mathématique, en particulier dans le calcul des prédicats ; les BDDs (pour Binary Decision Diagrams) sont des représentations de formules booléennes qui ont l'avantage d'être parfois exponentiellement plus compactes que les formules explicites qu'ils représentent.