zbMATH — the first resource for mathematics

Abstract diagnosis of functional programs. (English) Zbl 1278.68056
Leuschel, Michael (ed.), Logic based program synthesis and transformation. 12th international workshop, LOPSTR 2002, Madrid, Spain, September 17–20, 2002. Revised selected papers. Berlin: Springer (ISBN 3-540-40438-4/pbk). Lecture Notes in Computer Science 2664, 1-16 (2003).
Summary: We present a generic scheme for the declarative debugging of functional programs modeled as term rewriting systems. We associate to our programs a semantics based on a (continuous) immediate consequence operator, \(T_{\mathcal{R}}\), which models the (values/normal forms) semantics of \(\mathcal{R}\). Then, we develop an effective debugging methodology which is based on abstract interpretation: by approximating the intended specification of the semantics of \(\mathcal{R}\) we derive a finitely terminating bottom-up diagnosis method, which can be used statically. Our debugging framework does not require the user to either provide error symptoms in advance or answer questions concerning program correctness. We have made available a prototypical implementation in Haskell and have tested it on some non-trivial examples.
For the entire collection see [Zbl 1045.68013].

68N18 Functional programming and lambda calculus
68Q42 Grammars and rewriting systems
PDF BibTeX Cite
Full Text: DOI