Size-change termination and bound analysis

James Emil Avery

doi:10.1007/11737414_14

Size-change termination and bound analysis

James Emil Avery

Datalogisk Institut

16 Citationer (Scopus)

Abstract

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 http://esct.kvante.org), as well as for the ANSI C specializer C-Mix/ii, handling a subset of its internal language Core-C.

Originalsprog	Engelsk
Titel	Functional and Logic Programming : 8th International Symposium, FLOPS 2006, Fuji-Susono, Japan, April 24-26, 2006. Proceedings
Redaktører	Masami Hagiya, Philip Wadler
Antal sider	16
Forlag	Springer
Publikationsdato	2006
Sider	192-207
ISBN (Trykt)	978-3-540-33438-5
ISBN (Elektronisk)	978-3-540-33439-2
DOI	https://doi.org/10.1007/11737414_14
Status	Udgivet - 2006
Begivenhed	8th International Symposium on Functional and Logic Programming - Fuji-Susono, Japan Varighed: 24 apr. 2006 → 26 apr. 2006 Konferencens nummer: 8

Konference

Konference	8th International Symposium on Functional and Logic Programming
Nummer	8
Land/Område	Japan
By	Fuji-Susono
Periode	24/04/2006 → 26/04/2006

Navn	Lecture notes in computer science
Vol/bind	3945
ISSN	0302-9743

Emneord

Det Natur- og Biovidenskabelige Fakultet
automatisk programanalyse
termineringsanalyse
size-change grafer
size-change termineringsanalyse
konvekse polyeder
konvekse hylstre
abstrakt fortolkning

Adgang til dokumentet

10.1007/11737414_14

Citationsformater

Size-change termination and bound analysis. / Avery, James Emil.

Functional and Logic Programming: 8th International Symposium, FLOPS 2006, Fuji-Susono, Japan, April 24-26, 2006. Proceedings. red. / Masami Hagiya; Philip Wadler. Springer, 2006. s. 192-207 (Lecture notes in computer science, Bind 3945).

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

Avery, JE 2006, Size-change termination and bound analysis. i M Hagiya & P Wadler (red), Functional and Logic Programming: 8th International Symposium, FLOPS 2006, Fuji-Susono, Japan, April 24-26, 2006. Proceedings. Springer, Lecture notes in computer science, bind 3945, s. 192-207, 8th International Symposium on Functional and Logic Programming, Fuji-Susono, Japan, 24/04/2006. https://doi.org/10.1007/11737414_14

@inproceedings{bf3018d075ab11dcbee902004c4f4f50,

title = "Size-change termination and bound analysis",

abstract = "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 http://esct.kvante.org), as well as for the ANSI C specializer C-Mix/ii, handling a subset of its internal language Core-C.",

keywords = "Faculty of Science, automatisk programanalyse, termineringsanalyse, size-change grafer, size-change termineringsanalyse, konvekse polyeder, konvekse hylstre, abstrakt fortolkning, automatic program analysis, termination analysis, size-change graphs, size-change termination analysis, convex polyhedra, convex hulls, abstract interpretation",

author = "Avery, {James Emil}",

year = "2006",

doi = "10.1007/11737414_14",

language = "English",

isbn = "978-3-540-33438-5",

series = "Lecture notes in computer science",

publisher = "Springer",

pages = "192--207",

editor = "Masami Hagiya and Philip Wadler",

booktitle = "Functional and Logic Programming",

note = "8th International Symposium on Functional and Logic Programming ; Conference date: 24-04-2006 Through 26-04-2006",

}

TY - GEN

T1 - Size-change termination and bound analysis

AU - Avery, James Emil

N1 - Conference code: 8

PY - 2006

Y1 - 2006

N2 - 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 http://esct.kvante.org), as well as for the ANSI C specializer C-Mix/ii, handling a subset of its internal language Core-C.

AB - 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 http://esct.kvante.org), as well as for the ANSI C specializer C-Mix/ii, handling a subset of its internal language Core-C.

KW - Faculty of Science

KW - automatisk programanalyse

KW - termineringsanalyse

KW - size-change grafer

KW - size-change termineringsanalyse

KW - konvekse polyeder

KW - konvekse hylstre

KW - abstrakt fortolkning

KW - automatic program analysis

KW - termination analysis

KW - size-change graphs

KW - size-change termination analysis

KW - convex polyhedra

KW - convex hulls

KW - abstract interpretation

U2 - 10.1007/11737414_14

DO - 10.1007/11737414_14

M3 - Article in proceedings

SN - 978-3-540-33438-5

T3 - Lecture notes in computer science

SP - 192

EP - 207

BT - Functional and Logic Programming

A2 - Hagiya, Masami

A2 - Wadler, Philip

PB - Springer

T2 - 8th International Symposium on Functional and Logic Programming

Y2 - 24 April 2006 through 26 April 2006

ER -