PLT Redex is a domain-specific language designed for specifying and debugging operational semantics. Write down a grammar and the reduction rules, and PLT Redex allows you to interactively explore terms and to use randomized test generation to attempt to falsify properties of your semantics.
PLT Redex is embedded in Racket, meaning all of the convenience of a modern programming language is available, including standard libraries (and non-standard ones) and a program-development environment.
Getting started: Install Racket, start up DrRacket, and start your program with this:
Book: Semantics Engineering with PLT Redex (SEwPR) by Matthias Felleisen, Robby Findler, and Matthew Flatt gives the mathematical background for operational semantics, as well as a tutorial introduction to Redex. The preface, table of contents, and an example syllabus are available online. The book is available from MIT Press.
Documentation: The reference manual contains all of the gory details of all of Redex's operators.
Original PLT Redex publication: A paper on an early version of PLT Redex appeared at the International Conference on Rewriting Techniques and Applications (RTA) in 2004. Beware: the notations are different now (and there were fewer features back then); SEwPR is a better introduction to the system.