摘要：Graphical abstractDisplay OmittedAbstractProgram 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 setAof system assertions, in a Maude programRthat might disprove some of the assertions. The outcome of the technique is a safe program refinementR'ofRin which every computation is a good run, i.e., it satisfies the assertions inA. Furthermore, the transformation ensures that no good run ofRis removed fromR'. 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.
关键词：Assertion enforcement;Automated program transformation;Program repair;Equational rewriting;Rewriting logic, Maude
