A Smalltalk evolving algebra and its uses
George Robert Blakely · 1992
In his paper Logic and the Challenge of Computer Science (in Trends in Theoretical Computer Science, E. Borger, ed., Computer Science Press, 1988), Gurevich introduced a new algebraic operational formalism for describing program and programming language semantics. This formalism is based on evolving algebras. Evolving algebras have been developed to describe the semantics of Pascal, Modula-2, Occam, Prolog, and C. This thesis introduces the Pelops language as a vehicle for describing deterministic sequential evolving algebras. Pelops is used to describe an evolving algebra which captures the semantics of Mumble (a subset of Smalltalk). The description of Mumble supports Gurevich's New Thesis. A Hoare-style proof system for Pelops was developed to assist in reasoning about evolving algebras; this proof system is presented and proven sound. Novel features of the proof system include an axiom for reasoning about assignment to any closed term, and axioms for reasoning about storage allocation and deallocation. Several examples of the use of the proof system are presented, including some derivations of proof constructs for Mumble statements from the Pelops proof system and the Mumble evolving algebra. The intended audience for this thesis is computer scientists interested in evolving algebras, Gurevich's New Thesis, and the relationship between algebraic operational semantics and axiomatic semantics.