Un 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.
Pour s'assurer qu'un algorithme est correct, il faut démontrer deux choses: il faut démontrer que l'algorithme se termine (terminaison), autrement dit qu'il ne boucle pas ou ne diverge pas, produisant au moins un résultat et que le résultat de l'algorithme est effectivement de la forme énoncée par la spécification (correction partielle). La conjonction de la correction partielle et de la terminaison s'appelle la correction totale.
Comme la construction essentielle d'un algorithme itératif est la boucle (construction tant que ou while), l'argument principal de la démonstration de la correction partielle d'un algorithme itératif est la recherche d'un invariant pour chaque boucle (un invariant de boucle). Un invariant est un prédicat portant sur les variables du programme et sur des variables auxiliaires (ajoutées pour exprimer ce prédicat). La recherche des invariants est une opération difficile qui peut faire sortir de la logique utilisée pour décrire l'algorithme (incomplétude). Une fois ces invariants exhibés, le cœur de la démonstration consiste à démontrer que chaque invariant est effectivement stable lors de l'exécution de la boucle ; cela signifie que si l'invariant est satisfait avant l'exécution du corps de la boucle, il est satisfait après.
Algorithme récursif#Le problème de la correction partielle
Pour démontrer la correction d'un algorithme récursif, il faut connaître une précondition (un prédicat satisfait avant l'appel de l'algorithme) et une postcondition (un prédicat satisfait après l'appel de l'algorithme).
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.
Learn how to design and implement reliable, maintainable, and efficient software using a mix of programming skills (declarative style, higher-order functions, inductive types, parallelism) and
fundam
A hands-on introduction to interactive theorem proving, proofs as programs, dependent types, and to the Coq proof assistant. Come learn how to write bug-free code!
We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to u
Se concentre sur l'utilisation d'Inox pour la vérification des programmes, en démontrant le processus de vérification des programmes et en assurant l'exactitude.
In computer science, formal specifications are mathematically based techniques whose purpose are to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verifying key properties of interest through rigorous and effective reasoning tools. These specifications are formal in the sense that they have a syntax, their semantics fall within one domain, and they are able to be used to infer useful information.
La terminaison est une propriété fondamentale des algorithmes. Elle stipule que les calculs décrits par l'algorithme s'arrêteront. En général cet arrêt doit avoir lieu quelles que soient les données initiales que l'on fournit à l'algorithme. Si l'on veut insister sur ce point on parle alors souvent de terminaison uniforme, mais le plus généralement « terminaison » couvre aussi bien l'arrêt sur une donnée que l'arrêt sur toutes les données et c'est le contexte qui décide.
En informatique, le raffinement consiste à détailler la conception pour arriver par itérations à l'implémentation finale. À chaque itération correspond un niveau de granularité de plus en plus fin. Quand cette technique est appliquée au code source, la conception est alors matérialisée par du pseudo-code. Cette technique peut aussi être appliquée au modèle de données.
Under periodic lean/rich operation generated by repeated O2 pulses (O2-dithering), the abatement of CH4 and NO is enhanced compared to static operation. However, it is not well understood how the dithering parameters (pulse amplitude and frequency) affect ...
Automatic verification of programs manipulating arrays relies on specialised decision procedures. A methodology to classify the theories handled by these procedures is introduced. It is based on decomposition theorems in the style of Feferman and Vaught. T ...
Grading student SQL queries manually is a tedious and error-prone process. Earlier work on testing correctness of student SQL queries, such as the XData system, can be used to test the correctness of a student query. However, in case a student query is fou ...