Correct and complete (positive) strategy annotations for OBJ


María Alpuente, Santiago Escobar, and Salvador Lucas


Strategy annotations are used in several programming languages as replacement restrictions aimed at improving efficiency and/or reducing the risk of nontermination. Unfortunately, rewriting restrictions can have a negative impact on the ability to compute normal forms. In this paper, we first ascertain/clarify the conditions ensuring correctness and completeness (regarding normalization) of computing with strategy annotations. Then, we define a program transformation methodology for (correct and) complete evaluations which applies to OBJ-like languages.


Declarative programming, OBJ, strategy annotations.