Result: Size-change termination and bound analysis

Title:
Size-change termination and bound analysis
Authors:
AVERY, James
Source:
Functional and logic programming (8th international symposium, FLOPS 2006, Fuji-Susono, Japan, April 24-26, 2006)0FLOPS 2006. :192-207
Publisher Information:
Berlin: Springer, 2006.
Publication Year:
2006
Physical Description:
print, 3/4 p 1
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Sciences exactes et technologie, Exact sciences and technology, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Informatique théorique, Theoretical computing, Fonctions logiques, booléennes et de commutation, Logical, boolean and switching functions, Interprétation abstraite, Abstract interpretation, Interpretación Abstracta, Langage C, C language, Lenguaje C, Polyèdre, Polyhedron, Poliedro, Problème terminaison, Termination problem, Problema terminación, Programmation fonctionnelle, Functional programming, Programación funcional, Programmation logique, Logical programming, Programación lógica, Relation ordre partiel, Partial ordering, Relación orden parcial, Type donnée, Data type, Tipo dato, Analyse terminaison, Termination analysis, Análisis terminación
Document Type:
Conference Conference Paper
File Description:
text
Language:
English
Author Affiliations:
Dep. of Computer Science, University of Copenhagen (DIKU), Denmark
ISSN:
0302-9743
Access URL:
http://pascal-francis.inist.fr/vibad/index.php?action=search&terms=19105394
Rights:
Copyright 2007 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems
Accession Number:
edscal.19105394
Database:
PASCAL Archive

Further Information

Despite its simplicity, the size-change termination principle, presented by Lee, Jones and Ben-Amram in [LJB01], is surprisingly strong and is able to show termination for a large class of programs. A significant limitation for its use, however, is the fact that the SCT requires data types to be well-founded, and that all mechanisms used to determine termination must involve decreases in these global, well-founded partial orders. Following is an extension of the size-change principle that allows for non-well founded data types, and a realization of this principle for integer data types. The extended size-change principle is realized through combining abstract interpretation over the domain of convex polyhedra with the use of size-change graphs. In the cases when data types are well founded, the method handles every case that is handled by LJB size-change termination. The method has been implemented in a subject language independent shared library, libesct (available at [Ave05a]), as well as for the ANSI C specializer c-MixII, handling a subset of its internal language Core-C.