Transition between different abstraction levels in an abstract state machine (ASM) ground model

摘要

Kubovy et al. propose an interesting use of abstract state machines to automate elements of the software development process. The paper assumes prior knowledge of abstract state machines. Abstract state machines were originally introduced by Yuri Gurevich under the name "evolving algebras" in the early 1990s, and were subsequently developed by Blass, Gurevich, Borger and many others. Like other algebraic and logical structures, an abstract state machine has a signature, whose terms are built up recursively from variables and function symbols. Each term in an abstract state machine is viewed as defining a location, and each abstract state associates values from an underlying base set with locations. A state transition is made when that association is updated.