Verification of CRWL Programs with Rewriting Logic

José Miguel Cleva (Universidad Complutense de Madrid, Spain)

Isabel Pita (Universidad Complutense de Madrid, Spain)

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 approaches, is that it does not confuse the original functional-logic program with the subjects we want to talk about in the properties, but it allows the equational definition of observations on top of the transformed programs which simplifies the obtained proofs.

Keywords: Maude, functional logic programming, rewriting logic, verification

Categories: D.1.1, D.1.6, F.3.1