Bounding the Computational Complexity of Flowchart Programs with Multi-dimensional Rankings

Abstract : Proving the termination of a flowchart program can be done by exhibiting a ranking function, i.e., a function from the program states to a well-founded set, which strictly decreases at each program step. A standard method to automatically generate such a function is to compute invariants for each program point and to search for a ranking in a restricted class of functions that can be handled with linear programming techniques. Our first contribution is to propose an efficient algorithm to compute ranking functions: It can handle flowcharts of arbitrary structure, the class of candidate rankings it explores is larger, and our method, although greedy, is provably complete. Our second contribution is to show how to use the ranking functions we generate to get upper bounds for the computational complexity (number of transitions) of the source program, again for flowcharts of arbitrary structure. This estimate is a polynomial, which means that we can handle programs with more than linear complexity. We applied the method on a collection of test cases from the literature. We also point out important extensions, mainly to do with the scalability of the algorithm and, in particular, the integration of techniques based on cutpoints.
Type de document :
[Research Report] RR-7235, INRIA. 2010, pp.32
Liste complète des métadonnées

Littérature citée [33 références]  Voir  Masquer  Télécharger
Contributeur : Christophe Alias <>
Soumis le : mardi 16 mars 2010 - 18:53:58
Dernière modification le : jeudi 22 novembre 2018 - 12:50:02
Document(s) archivé(s) le : vendredi 18 juin 2010 - 23:26:25


Fichiers produits par l'(les) auteur(s)


  • HAL Id : inria-00464356, version 1


Christophe Alias, Alain Darte, Paul Feautrier, Laure Gonnord. Bounding the Computational Complexity of Flowchart Programs with Multi-dimensional Rankings. [Research Report] RR-7235, INRIA. 2010, pp.32. 〈inria-00464356〉



Consultations de la notice


Téléchargements de fichiers