(AMN) A language for specifying abstract machines in the b-method, based on the mathematical theory of generalised substitutions.