Catalogo Articoli (Spogli Riviste)

OPAC HELP

Titolo:
The size-change principle for program termination
Autore:
Lee, CS; Jones, ND; Ben-Amram, AM;
Indirizzi:
Univ Copenhagen, Datalog Inst, DK-2100 Copenhagen, Denmark Univ Copenhagen Copenhagen Denmark DK-2100 , DK-2100 Copenhagen, Denmark Acad Coll Tel Aviv Yaffo, IL-64044 Tel Aviv, Israel Acad Coll Tel Aviv Yaffo Tel Aviv Israel IL-64044 64044 Tel Aviv, Israel Univ Western Australia, Dept Comp Sci & Software Engn, Nedlands, WA 6907, Australia Univ Western Australia Nedlands WA Australia 6907 nds, WA 6907, Australia
Titolo Testata:
ACM SIGPLAN NOTICES
fascicolo: 3, volume: 36, anno: 2001,
pagine: 81 - 92
SICI:
1523-2867(200103)36:3<81:TSPFPT>2.0.ZU;2-#
Fonte:
ISI
Lingua:
ENG
Keywords:
termination; program analysis; omega automaton; PSPACE-completeness; partial evaluation;
Tipo documento:
Article
Natura:
Periodico
Settore Disciplinare:
Engineering, Computing & Technology
Citazioni:
20
Recensione:
Indirizzi per estratti:
Indirizzo: Lee, CS Univ Western Australia, Dept Comp Sci & Software Engn, Nedlands, WA 6907, Australia Univ Western Australia Nedlands WA Australia 6907 6907, Australia
Citazione:
C.S. Lee et al., "The size-change principle for program termination", ACM SIGPL N, 36(3), 2001, pp. 81-92

Abstract

The "size-change termination" principle for a first-order functional language with well-founded data is: a program terminates on all inputs if every infinite call sequences (following program control flow) would cause an infinite descent in some data values. Size-change analysis is based only on local approximations to parameter size changes derivable from program syntax. The set of infinite call sequences that follow program flow and can be recognized as causing infinite descent is an w-regular set, representable by a Buchi automaton. Algorithms for such automata can be used to decide size-change termination. We also give a direct algorithm operating on "size-change graphs" (without the passage to automata). Compared to other results in the literature, termination analysis based onthe size-change principle is surprisingly simple and general: lexical orders (also called lexicographic orders), indirect function calls and permutedarguments (descent that is not in-situ) are all handled automatically and without special treatment, with no need for manually supplied argument orders, or theorem-proving methods not certain to terminate at analysis time. We establish the problem's intrinsic complexity. This turns out to be surprisingly high, complete for PSPACE, in spite of the simplicity of the principle. PSPACE hardness is proved by a reduction from Boolean program termination. An interesting consequence: the same hardness result applies to many other analyses found in the termination and quasi-termination literature.

ASDD Area Sistemi Dipartimentali e Documentali, Università di Bologna, Catalogo delle riviste ed altri periodici
Documento generato il 27/05/20 alle ore 15:07:12