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...

• Type: Journal
• Year: 2006
• Where: JUCS
• Authors: José Miguel Cleva, Isabel Pita
• Keywords: Functional-logic Program, JUCS 2006, Logic Logical Framework, Rewriting Logic