Transformations of Evolving Algebras

. We give a precise definition of evolving algebras as nondeterministic, mathematical machines. All proofs in the paper are based on this definition. First we define constant propagation. We extend evolving algebras by macros and define folding and unfolding transformations. Next we introduce a simple transformation to flatten transition rules. Finally a pass separation transformation for evolving algebras is presented. It can be used to derive a compiler and abstract machine from an interpreter. All transformations are proven correct. Finally a comparison to other work is given. 1 Introduction Evolving algebras (EvAs) have been proposed by Gurevich in [Gur91] and used by Gurevich and others to give the operational semantics of languages like C, Modula2, Prolog and Occam. Borger and Rosenzweig's proof of the correctness of the Warren Abstract Machine is based on a slight variation of evolving algebras ([BR92]). An evolving algebra may be tailored to the abstraction level necessary for..