Concept
Méthode formelle (informatique)
Concepts associés (23)
Langage de spécification
Un langage de spécification est un Langage formel en Informatique utilisé pendant l'analyse systémique, l'analyse des exigences et la conception des systèmes pour décrire un système à un niveau beaucoup plus élevé qu'un langage de programmation, qui est utilisé pour produire un code exécutable pour un système. Les langages de spécification ne sont généralement pas exécutés directement. Ils sont destinés à décrire le quoi, pas le comment. En effet, il est considéré comme une erreur si une spécification d'exigence est encombrée de détail d'implémentation non nécessaire.
Type system
In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type (for example, integer, floating point, string) to every "term" (a word, phrase, or other set of symbols). Usually the terms are various constructs of a computer program, such as variables, expressions, functions, or modules. A type system dictates the operations that can be performed on a term. For variables, the type system determines the allowed values of that term.
Analyse statique de programmes
En informatique, la notion d’analyse statique de programmes couvre une variété de méthodes utilisées pour obtenir des informations sur le comportement d'un programme lors de son exécution sans réellement l'exécuter. C'est cette dernière restriction qui distingue l'analyse statique des analyses dynamiques (comme le débugage ou le profiling) qui s'attachent, elles, au suivi de l’exécution du programme. L’analyse statique est utilisée pour repérer des erreurs formelles de programmation ou de conception et pour déterminer la facilité ou la difficulté à maintenir le code.
Informatique théorique
vignette|Une représentation artistique d'une machine de Turing. Les machines de Turing sont un modèle de calcul. L'informatique théorique est l'étude des fondements logiques et mathématiques de l'informatique. C'est une branche de la science informatique et la science formelle. Plus généralement, le terme est utilisé pour désigner des domaines ou sous-domaines de recherche centrés sur des vérités universelles (axiomes) en rapport avec l'informatique.
Vérification formelle
In 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.
Haskell
Haskell est un langage de programmation fonctionnel fondé sur le lambda-calcul et la logique combinatoire. Son nom vient du mathématicien et logicien Haskell Curry. Il a été créé en 1990 par un comité de chercheurs en théorie des langages intéressés par les langages fonctionnels et l'évaluation paresseuse. Le dernier standard est Haskell 2010 : c'est une version minimale et portable du langage conçue à des fins pédagogiques et pratiques, dans un souci d'interopérabilité entre les implémentations du langage et comme base de futures extensions.
Sémantique des langages de programmation
En 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.
Programmation par contrat
La programmation par contrat (en anglais, design by contract ou DBC) est un paradigme de programmation dans lequel le déroulement des traitements est régi par des règles. Ces règles, appelées des assertions, forment un contrat qui précise les responsabilités entre le client et le fournisseur d'un morceau de code logiciel. C'est une méthode de programmation semi-formelle dont le but principal est de réduire le nombre de bugs dans les programmes.
Interprétation abstraite
L'interprétation abstraite est une théorie d'approximation de la sémantique de programmes informatiques fondée sur les fonctions monotones pour ensembles ordonnés, en particulier les treillis (en anglais : lattice). Elle peut être définie comme une exécution partielle d'un programme pour obtenir des informations sur sa sémantique (par exemple, sa structure de contrôle, son flot de données) sans avoir à en faire le traitement complet.
Sémantique opérationnelle
En informatique, la sémantique opérationnelle est l'une des approches qui servent à donner une signification aux programmes informatiques d'une manière rigoureuse, mathématiquement parlant (voir Sémantique des langages de programmation). Une sémantique opérationnelle d'un langage de programmation particulier décrit comment chaque programme valide du langage doit être interprété en termes de suite d'états successifs dans la machine. Cette suite d'états est la signification du programme.