  We propose B Maude, a prototype executable environment for the Abstract
Machine Notation implemented in the Maude language. B Maude is formally defined
and results from the implementation of the semantics of AMN as denotations in
the $\pi$ Framework, a realization of Mosses' Component-based Semantics and
Plotkin's Interpreting Automata. B Maude endows the B method with execution by
rewriting, symbolic search with narrowing and Linear Temporal Logic model
checking of AMN descriptions.
