Correction d'un algorithme | EPFL Graph Search

Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?

Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur GraphSearch.

Découvrez-en plus sur les applications Graph.

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).

À propos de ce résultat

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.

Publications associées (2)

Personnes associées (1)

Concepts associés (15)

Cours associés (5)

Séances de cours associées (57)

CS-214: Software construction

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

CS-628: Interactive Theorem Proving CS

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!

CS-550: Formal verification

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

ScalaDyno: Making Name Resolution and Type Checking Fault-tolerant

Martin Odersky, Vlad Ureche, Cédric Bastin

The ScalaDyno compiler plugin allows fast prototyping with the Scala programming language, in a way that combines the benefits of both statically and dynamically typed languages. Static name resolution and type checking prevent partially-correct code from being compiled and executed. Yet, allowing programmers to test critical paths in a program without worrying about the consistency of the entire code base is crucial to fast prototyping and agile development. This is where ScalaDyno comes in: it allows partially-correct programs to be compiled and executed, while shifting compile-time errors to program runtime. The key insight in ScalaDyno is that name and type errors affect limited areas of the code, which can be replaced by instructions to output the respective errors at runtime. This allows byte code generation and execution for partially correct programs, thus allowing Python or JavaScript-like fast prototyping in Scala. This is all done without sacrificing name resolution, full type checking and optimizations for the correct parts of the code -- they are still performed, but without getting in the way of agile development. Finally, for release code or sensitive refactoring, runtime errors can be disabled, thus allowing full static name resolution and type checking typical of the Scala compiler.

ACM2014

We review adaptive Markov chain Monte Carlo algorithms (MCMC) as a mean to optimise their performance. Using simple toy examples we review their theoretical underpinnings, and in particular show why adaptive MCMC algorithms might fail when some fundamental properties are not satisfied. This leads to guidelines concerning the design of correct algorithms. We then review criteria and the useful framework of stochastic approximation, which allows one to systematically optimise generally used criteria, but also analyse the properties of adaptive MCMC algorithms. We then propose a series of novel adaptive algorithms which prove to be robust and reliable in practice. These algorithms are applied to artificial and high dimensional scenarios, but also to the classic mine disaster dataset inference problem.

2008

Correction d'un algorithme

Formal specification

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.

Terminaison d'un algorithme

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.

Intégrité du noyau et systèmes en temps réel

Explore l'intégrité du noyau, la sécurité du système et la vérification du système en temps réel, en soulignant l'importance de prouver les propriétés critiques pour la construction de systèmes sécurisés et opportuns.

Vérification automatique des exercices de programmation

Couvre un cadre pour la vérification automatique des exercices de programmation, y compris le traitement axiomatique et la représentation par modèle.

Tutoriel en acier inoxydable: Vérification du code Scala CS-550: Formal verification

Couvre l'utilisation de Stainless, un outil de vérification pour Scala, pour assurer l'exactitude du code Scala.