Termination of programs with strategy annotations
Author
Salvador Lucas
Abstract
Strategy annotations have been
used in a number of programming languages and rewriting-based systems
(e.g., OBJ2, OBJ3, CafeOBJ, Maude, JITty, µCRL, ...) for improving
the termination behavior and avoiding useless
computations. Regarding the ability of these annotations to improve
the termination behavior of programs, the possibility of forbidding
reductions on some arguments of function symbols play a crucial role.
From an abstract point of view, in term rewriting this feature has
been modeled as the so-called context-sensitive rewriting (CSR).
We show that CSR
provides a framework for analyzing termination of programs running
under control of strategy annotations. Thus, CSR and its
associated techniques for ensuring termination
provide a useful tool for the programmers and designers of software
systems aimed at supporting the practical use of such programming
languages and rewriting-based systems.
Keywords
CafeOBJ, Maude, OBJ, program annotations,
programming languages, programmable strategies,
term rewriting, termination.