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).
Sémantique dénotationnelleEn informatique, la sémantique dénotationnelle est une des approches permettant de formaliser la signification d'un programme en utilisant les mathématiques. Parmi les autres approches, on trouve la sémantique axiomatique et la sémantique opérationnelle. Cette discipline a été introduite par Christopher Strachey et Dana Scott. En général, la sémantique dénotationnelle utilise des techniques de programmation fonctionnelle pour décrire les langages informatiques, les architectures et les programmes.
Program analysisIn computer science, program analysis is the process of automatically analyzing the behavior of computer programs regarding a property such as correctness, robustness, safety and liveness. Program analysis focuses on two major areas: program optimization and program correctness. The first focuses on improving the program’s performance while reducing the resource usage while the latter focuses on ensuring that the program does what it is supposed to do.
Logique de HoareLa logique de Hoare, parfois appelée logique de Floyd-Hoare, est une méthode formelle définie par le chercheur en informatique britannique Tony Hoare dans un article de 1969 intitulé An Axiomatic Basis for Computer Programming. La méthode de Hoare met en place un formalisme logique permettant de raisonner sur la correction des programmes informatiques. Elle est fondée sur la syntaxe en ce sens que la correction d'un programme est décrite et démontrée par induction (récurrence) sur la structure du programme : à chaque règle syntaxique de construction d'un programme correspond une règle de la logique de Hoare.
Vérification formelleIn the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code.
Vérification de modèlesthumb|308x308px|Principe du model checking. En informatique, la vérification de modèles, ou model checking en anglais, est le problème suivant : vérifier si le modèle d'un système (souvent informatique ou électronique) satisfait une propriété. Par exemple, on souhaite vérifier qu'un programme ne se bloque pas, qu'une variable n'est jamais nulle, etc. Généralement, la propriété est écrite dans un langage, souvent en logique temporelle. La vérification est généralement faite de manière automatique.
Correction d'un algorithmeUn algorithme est correct s'il fait ce qu'on attend de lui. Plus précisément, rappelons qu'un algorithme est décrit par une spécification des données sur lesquelles l'algorithme va démarrer son calcul et une spécification du résultat produit par l'algorithme. Démontrer la correction de l'algorithme consiste à démontrer que l'algorithme retourne, quand il calcule en partant des données, un objet qui est un des résultats escomptés et qui satisfait la spécification du résultat comme énoncé dans la description de l'algorithme.
Bug (informatique)vignette|upright=1|Le Mac triste : écran indiquant un code erreur sur les premières versions du MacIntosh d'Apple. En informatique, un bug (prononcé en français : ) ou bogue est un défaut de conception d'un programme informatique à l'origine d'un dysfonctionnement. La gravité du dysfonctionnement peut aller de bénigne, causant par exemple des défauts d'affichage mineurs à majeure, tels un plantage du système pouvant entraîner de graves accidents, par exemple la destruction en vol de la première fusée Ariane 5, en 1996.
Sémantique des langages de programmationEn informatique théorique, la sémantique formelle (des langages de programmation) est l’étude de la signification des programmes informatiques vus en tant qu’objets mathématiques. Comme en linguistique, la sémantique, appliquée aux langages de programmation, désigne le lien entre un signifiant, le programme, et un signifié, objet mathématique. L'objet mathématique dépend des propriétés à connaître du programme. La sémantique est également le lien entre : le langage signifiant : le langage de programmation le langage signifié : logique de Hoare, automates.
Test (informatique)vignette|Une programmeuse écrivant du code Java avec JUnit. En informatique, un test désigne une procédure de vérification partielle d'un système. Son objectif principal est d'identifier un nombre maximal de comportements problématiques du logiciel. Il permet ainsi, dès lors que les problèmes identifiés seront corrigés, d'en augmenter la qualité. D'une manière plus générale, le test désigne toutes les activités qui consistent à rechercher des informations quant à la qualité du système afin de permettre la prise de décisions.
