Static Correction of Maude Programs
with Assertions

We present a novel transformation method for Maude programs featuring both automatic program diagnosis and correction. The input of our method is a reference specification of the program behavior that is given in the form of a set A of system assertions, and an overly general program R that may produce some undesired computations which violate the assertions. Our technique translates R into a refined program R' in which every computation satisfies the assertions of A. Our correction technique is first formalized for topmost rewrite theories, and then we generalize it to larger rewrite theories that support nested structured configurations. Our technique supports assertional specifications and is static, hence it does not require the knowledge of any failing run, and we cope with infinite space states. We report experiments that provide a preliminary assessment of the effectiveness of assertion-driven Maude program correction.