Abstract
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 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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
J. R. Abrial. The B-Book. Assigning Programs to Meanings. Cambridge University Press, 1996.
M. Anlauff. XASM-An extensible, component-based Abstract State Machines language. In Y. Gurevich, M. Odersky, and L. Thiele, editors, Proc. ASM 2000, Lecture Notes in Computer Science. Springer-Verlag, 2000. to appear.
C. Böhm and G. Jacopini. Flow diagrams, Turing Machines, and languages with only two formation rules. Communications of the ACM, 9(5):366–371, 1966.
E. Börger. High level system design and analysis using Abstract State Machines. In D. Hutter, W. Stephan, P. Traverso, and M. Ullmann, editors, Current Trends in Applied Formal Methods (FM-Trends 98), number 1641 in Lecture Notes in Computer Science, pages 1–43. Springer-Verlag, 1999.
E. Börger, A. Cavarra, and E. Riccobene. An ASM semantics for UML Activity Diagrams. In T. Rust, editor, Proc. AMAST 2000, Lecture Notes in Computer Science. Springer-Verlag, 2000.
E. Börger, A. Cavarra, and E. Riccobene. A simple formal model for UML State Machines. In Y. Gurevich, M. Odersky, and L. Thiele, editors, Proc. ASM 2000, Lecture Notes in Computer Science. Springer-Verlag, 2000. to appear.
E. Börger, E. Grädel, and Y. Gurevich. The Classical Decision Problem. Perspectives in Mathematical Logic. Springer-Verlag, 1997.
E. Börger, J. Schmid, W. Schulte, and R. Stärk. Java and the Java Virtual Machine. Lecture Notes in Computer Science. Springer-Verlag, 2000. to appear.
E. Börger and W. Schulte. Modular Design for the Java Virtual Machine Architecture. In E. Börger, editor, Architecture Design and Validation Methods, pages 297–357. Springer-Verlag, 2000.
A. Brüggemann, L. Priese, D. Rödding, and R. Schätz. Modular decomposition of automata. In E. Börger, G. Hasenjäger, and D. Rödding, editors, Logic and Machines: Decision Problems and Complexity, number 171 in Lecture Notes in Computer Science, pages 198–236. Springer-Verlag, 1984.
G. D. Castillo. ASM-SL, a Specification Language based on Gurevich’s Abstract State Machines, 1999.
M. Davis. The Universal Computer: The Road from Leibniz to Turing. W.W. Norton, New York, 2000. to appear.
Y. Gurevich. Evolving Algebras 1993: Lipari Guide. In E. Börger, editor, Specification and Validation Methods, pages 9–36. Oxford University Press, 1995.
Y. Gurevich. Sequential Abstract State Machines capture sequential algorithms. ACM Transactions on Computational Logic, 1(1), 2000.
Y. Gurevich and M. Spielmann. Recursive abstract state machines. Journal of Universal Computer Science, 3(4):233–246, 1997.
S. C. Kleene. Introduction to Metamathematics. D. van Nostrand, Princeton, New Jersey, 1952.
D. L. Parnas. Information distribution aspects of design methodology. In Information Processing 71, pages 339–344. North Holland Publishing Company, 1972.
J. Schmid. Executing ASM specifications with AsmGofer. Web pages at: http://www.tydo.de/AsmGofer, 1999.
A. Zamulin. Object-oriented Abstract State Machines. In Proceedings of the 28th Annual Conference of the German Society of Computer Science. Technical Report, Magdeburg University, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Börger, E., Schmid, J. (2000). Composition and Submachine Concepts for Sequential ASMs. In: Clote, P.G., Schwichtenberg, H. (eds) Computer Science Logic. CSL 2000. Lecture Notes in Computer Science, vol 1862. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44622-2_3
Download citation
DOI: https://doi.org/10.1007/3-540-44622-2_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67895-3
Online ISBN: 978-3-540-44622-4
eBook Packages: Springer Book Archive