Using Rewriting Logic to specify program semantics

An Executable Semantic Definition of the Beta Language using Rewriting Logic.

Rewriting logic specifications are an attempt to provide easy and expressive ways to develop executable formal definitions of languages. Among other benefits is that these can be analyzed by automated tools. The Maude Project is one of the main groups looking into rewriting logic specifications. The paper Twenty Years of Rewriting Logic is a good overview and summary.

BETA is an object-oriented programming language that numbers Simula-67 and Smalltalk among its spiritual ancestors. A 1993 book is now available in PDF: Object-Oriented Programming in the Beta Programming Language.