Composition and Submachine Concepts for Sequential ASMs

We define three composition and structuring concepts which reflect frequently used refinements of ASMs and integrate standard structuring constructs into the global state based parallel ASM view of computations. First we provide an operator which combines the atomic update view of ASMs with sequential machine execution and naturally incorporates classical iteration constructs into ASMs. For structuring large machines we define their parameterization, leading to a notion of possibly recursive submachine calls which sticks to the bare logical minimum needed for sequential ASMs, namely consistency of simultaneous machine 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 ASMGofer. 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 ...

• Type: Conference
• Year: 2000
• Where: CSL
• Authors: Egon Börger, Joachim Schmid
• Keywords: Automated Reasoning, Constructs, CSL 2000, Integrate Standard Structuring, Structuring