On Gurevich's theorem on sequential algorithms

Abstract-State Machines have been introduced as “a computation model that is more powerful and more universal than standard computation models”, by Yuri Gurevich in 1985. ASM gained much attention as a specification method, in particular for the description of the semantics of programming languages, communication protocols, distributed algorithms, etc. Gurevich proved recently that a sequential algorithm must only meet a few liberal requirements to be representable as an ASM. We critically examine Gurevich's requirements for sequential algorithms, as well as the semantics of ASM-programs and the proof of his main theorem. A couple of examples support and explain intuition and motivation of ASM.