Structure de données persistanteEn informatique, une structure de données persistante est une structure de données qui préserve ses versions antérieures lorsqu'elle est modifiée ; une telle structure est immuable, car ses opérations ne la modifient pas en place (de manière visible) mais renvoient au contraire de nouvelles structures. Une structure est partiellement persistante si seule sa version la plus récente peut être modifiée, les autres n'étant accessibles qu'en lecture. La structure est dite totalement persistante si chacune de ses versions peut être lue ou modifiée.
Structure de donnéesEn informatique, une structure de données est une manière d'organiser les données pour les traiter plus facilement. Une structure de données est une mise en œuvre concrète d'un type abstrait. Pour prendre un exemple de la vie quotidienne, on peut présenter des numéros de téléphone par département, par nom, par profession (comme les Pages jaunes), par numéro téléphonique (comme les annuaires destinés au télémarketing), par rue et/ou une combinaison quelconque de ces classements.
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.
Analyse statique de programmesEn 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.
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.
Purely functional data structureIn computer science, a purely functional data structure is a data structure that can be directly implemented in a purely functional language. The main difference between an arbitrary data structure and a purely functional one is that the latter is (strongly) immutable. This restriction ensures the data structure possesses the advantages of immutable objects: (full) persistency, quick copy of objects, and thread safety. Efficient purely functional data structures may require the use of lazy evaluation and memoization.
Type récursifEn programmation informatique et théorie des types, un type récursif est un type de données dont la définition fait appel au type lui‐même, de façon récursive. Cela permet entre autres des structures de données qui contiennent des sous‐structures du même type. Cette notion s'applique naturellement dans l'étude des listes et des arbres. Type algébrique de données Les types algébriques sont de loin la forme la plus courante de types récursifs. Un exemple classique est le type liste.
Tas (informatique)vignette|Un exemple de tas. Il contient 9 éléments. L'élément le plus prioritaire (100) est à la racine. En informatique, un tas (ou monceau au Canada, heap en anglais) est une structure de données de type arbre qui permet de retrouver directement l'élément que l'on veut traiter en priorité. C'est un arbre binaire presque complet ordonné. Un arbre binaire est dit presque complet si tous ses niveaux sont remplis, sauf éventuellement le dernier, qui doit être rempli sur la gauche (cf. Contre-exemples).
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.
Runtime verificationRuntime verification is a computing system analysis and execution approach based on extracting information from a running system and using it to detect and possibly react to observed behaviors satisfying or violating certain properties. Some very particular properties, such as datarace and deadlock freedom, are typically desired to be satisfied by all systems and may be best implemented algorithmically. Other properties can be more conveniently captured as formal specifications.
