Composition and submachine concepts for sequential ASMs

Abstract. We define three composition and structuring concepts which reflect frequently used refinements of ASMs and integrate standard struc-turing constructs into the global state based parallel ASM view of compu-tations. First we provide an operator which combines the atomic update view of ASMs with sequential machine execution and naturally incor-porates classical iteration constructs into ASMs. For structuring large machines we define their parameterization, leading to a notion of possi-bly recursive submachine calls which sticks to the bare logical minimum needed for sequential ASMs, namely consistency of simultaneous ma-chine operations. For encapsulation and state hiding we provide ASMs with local state, return values and error handling. Some of these structuring constructs have been implemented in ASM-Gofer. We provide also a proof-theoretic definition which supports the use of common structured proof principles for proving properties for complex machines in terms of properties of their components.