Preuve de terminaison de boucles: recueil de méthodes et application par l'exemple

Mémoire de de BORCHGRAVE d'ALTENA Florence

Actuellement, il existe une multitude de méthodes qui permettent de prouver la terminaison de boucles. Ce mémoire rassemble, explique et compare, souvent par l'exemple les principales de ces méthodes jugées les plus pertinentes. Notons que ces méthodes peuvent dans certains cas prouver qu'une boucle se terminera. Par contre, aucune d'entre elles n'est capable de prouver la terminaison de toutes les boucles. En effet, nous savons par Turing que la terminaison est un problème indécidable. La plupart des méthodes présentées dans ce mémoire se basent sur la démonstration de Turing prouvant que si une fonction de rang existe, alors la boucle correspondante se terminera. Chacune des méthodes actuelles représente une amélioration d'une méthode précédente. Il n'existe pas encore de méthode universelle.

Mots clés : Terminaison de boucles, méthode de Chen, fonction de rang, preuve de Turing

 

There are currently a high number of methods aiming to demonstrate the termination of a loop. This thesis summarizes, explains, -often by way of examples-, and compares the more important among these methods, those also judged to be the most relevant. Note that these methods may in some cases demonstrate that a loop terminates. However, none of them can prove the termination of every loop. Indeed we know from Turing that issue of loop termination cannot be decided. Most methods presented in this paper are based on the demonstration by Turing that if a ranking function exists, then the corresponding loop will terminate. Each of the current methods represents an improvement over another earlier method.  There is however no universal method.

%Currently, there are a multitude of methods to prove the termination of loops. This thesis brings explains, often by example and compares the main of these methods considered most relevant. Note that these methods may in some cases prove that a loop terminate. However, none of them is able to proof the termination of every the loops. Indeed, we know from Turing that termination is an undecidable problem. Most methods present in this thesis are based on the demonstration of Turing proving that if a ranking function exists, then the corresponding loop terminate. Current methods are each an improvement of another method there doesn't exist universal method.

Keywords : Loop termination, Chen's method, ranking function, Turing's proof

Contact : Debay Maïllis - 081/72.52.52 - secretariat.info@unamur.be
Télecharger : vCal