Abstract State Machine

From http://www.di.unipi.it/~boerger/ASMTutorialEtaps.html:

A sequential ASM is defined as a set of transition rules of form

if Condition then Updates

which transform first-order structures (the states of the machine), where the guard Condition, which has to be satisfied for a rule to be applicable, is a variable free first-order formula, and Updates is a finite set of function updates (containing only variable free terms) of form

  f (t1,...,tn) := t

The execution of these rules is understood as updating, in the given state and in the indicated way, the value of the function f at the indicated parameters, leaving everything else unchanged. (This proviso avoids the frame problem of declarative approaches.) In every state, all the rules which are applicable are simultaneously applied (if the updates are consistent) to produce the next state. If desired or useful, declarative features can be built into an ASM by integrity constraints and by assumptions on the state, on the environment, and on the applicability of rules.

---

SeeAlso FormalMethods