Sciweavers

JUCS
2006

Verification of CRWL Programs with Rewriting Logic

13 years 12 months ago
Verification of CRWL Programs with Rewriting Logic
Abstract: We present a novel approach to the verification of functional-logic programs. For our verification purposes, equational reasoning is not valid due to the presence of non-deterministic and partial functions. Our approach transforms functionallogic programs into Maude theories and then uses the Rewriting Logic logical framework to verify properties of the transformed programs. We propose an inductive proving method based on the length of the computation on the Rewriting Logic framework to cope with the non-deterministic and non-terminating aspects of the programs. We illustrate the application of the method on various examples, where we analyze the sequence of steps to be performed by the proof in order to get expertise for the automatization of the process. Then, since the proposed transformation process is also amenable of automatization, we will obtain a tool for proving properties of CRWL programs. Another advantage of our methodology, that distinguish it from other approac...
José Miguel Cleva, Isabel Pita
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2006
Where JUCS
Authors José Miguel Cleva, Isabel Pita
Comments (0)