Refinement and implementation techniques for Abstract State Machines
Joachim W. Schmid · OPen Access Repositorium der Universität Ulm (OPARU) (Ulm University) · 2002
This thesis introduces several structuring and composition principles for Abstract State Machines (ASMs). The concepts can be used to structure single machines (by using parametrized machines, sequential execution, iteration, local state e.g.) as well as to divide large specifications into simpler parts by using the introduced component concept. We discussed how to extend and modify a semantics for lazy evaluation in order to support dynamic functions and simultaneous function updates which are essential features in ASMs. Our semantics is not defined on top of a semantics for terms, because our aim is to extend an existing system for lazy evaluation according to the semantics extension. This new system is called AsmGofer and it is a conservative extension of TkGofer. AsmGofer is especially useful for executable specifications and their validation. Multi agent ASMs are supported, just as non-deterministic selection of elements and rules, sequential execution and iteration of rules, higher-order functions, recursive definitions for rules and functions, constructor classes, graphical user interfaces, etc. The tool was extensively used in the book Java and the Java Virtual Machine, where the ASM models for Java, the Java Virtual Machine, the Java Compiler, and the Bytecode Verifier are executable with AsmGofer.