Evolving algebras: Tools for specification, validation, and program transformation.

Abstract

We begin with an introduction to evolving algebras, presenting all the major constructs with numerous examples. We then present an evolving algebra for the C programming language in its entirety, presenting the semantics of C at four different layers of abstraction. This shows that real-life systems such as C can be described simply and elegantly. Continuing, we present a complete specification of the Kermit file transfer protocol, commonly used by many computer systems. We use this specification to give the first known proof of correctness for this protocol, using the natural layers of abstraction given in the protocol to create a layered proof. Finally, we describe the architecture of an evolving algebra partial evaluator, a program which specializes an evolving algebra with respect to a portion of its input. We discuss the particular analysis, specialization, and optimization techniques used and show an example of its use.