ASF+SDF

The technical infrastructure we will use for renovation is primarily based on the ASF+SDF Meta-Environment. The specification formalism ASF+SDF [3,29,19] is a combination of the algebraic specification formalism ASF and the syntax definition formalism SDF. ASF+SDF specifications consist of modules, each module has an SDF-part (defining lexical and context-free syntax) and an ASF-part (defining equations). The SDF part corresponds to signatures in ordinary algebraic specification formalisms. However, syntax is not restricted to plain prefix notation since arbitrary context-free grammars can be defined. The syntax defined in the SDF-part of a module can be used immediately when defining equations, the syntax in equations is thus user-defined. The equations in an ASF+SDF specification have the following distinctive features:

• Conditional equations with positive and negative conditions.
• Non left-linear equations.
• List matching.
• Default equations.

It is possible to execute specifications by interpreting the equations as conditional rewrite rules. The semantics of ASF+SDF is based on innermost rewriting. Default equations are tried when all other applicable equations have failed, because either the arguments did not match or one of the conditions failed.

One of the powerful features of the ASF+SDF specification language is list matching. The implementation of list matching may involve backtracking to find a match that satisfies the left-hand side of the rewrite rule as well as all its conditions. There is only backtracking within the scope of a rewrite rule, so if the right-hand side of the rewrite rule is normalized and this normalization fails no backtracking is performed to find a new match.

The development of ASF+SDF specifications is supported by an interactive programming environment, the ASF+SDF Meta-Environment [32]. In this environment specifications can be developed and tested. It provides syntax-directed editors, a parser generator, a pretty printer generator, and a rewrite engine. Given this rewrite engine terms can be reduced by interpreting the equations as rewrite rules. An overview of industrial applications of the system can be found in [6,10].