Specification language design concepts: Aggregation and extensibility in CoreASM

Abstract State Machines (ASMs) are a proven methodology for the precise high-level specification of formal requirements in early phases of software design. Many extensions to ASMs have been proposed and used widely, including Distributed ASMs, Turbo ASMs, Gurevich's partial updates, and syntactically convenient rule forms. This, coupled with the fact that ASMs do not bind the user to any predetermined data types or operators, allows for extreme flexibility in exploration of the problem space. Striving to provide this same level of freedom with executable ASMs, the CoreASM engine and language have been designed with syntactic and semantic extensibility in mind. We formally specify extensibility mechanisms that allow for language augmentation with arbitrary data structures supporting simultaneous incremental modification, new operators, and additional language syntax. Our work is a major step toward providing an environment suitable for both further experimentation with ASMs and for the machine-aided creation of robust software specifications.