Imposing Assertions in Maude via Program Transformation

Abstract

[EN] Program transformation is widely used for producing correct mutations of a given program so as to satisfy the user's intent that can be expressed by means of some sort of specification (e.g. logical assertions, functional specifications, reference implementations, summaries, examples). This paper describes an automated correction methodology for Maude programs that is based on program transformation and can be used to enforce a safety policy, given by a set A of system assertions, in a Maude program R that might disprove some of the assertions. The outcome of the technique is a safe program refinement R' of R in which every computation is a good run, i.e., it satisfies the assertions in A. Furthermore, the transformation ensures that no good run of R is removed from R'. Advantages of this correction methodology can be summarized as follows.

A fully automatic program transformation featuring both program diagnosis and repair that preserves all executability requirements.

A simple logical notation to declaratively express invariant properties and other safety constraints through assertions.

No dynamic information is required to infer program fixes: the methodology is static and does not need to collect any error symptom at runtime.