AsmL Semantics in Fixpoint.
Ali Habibi, Sofiène Tahar · 2005
Abstract. AsmL is a novel executable specification language based on the theory of Abstract State Machines (ASMs). It represents one of the most powerful practical engines to write and execute ASMs. In this pa-per, we present a proven complete small-step trace-based operational semantics of the main parts of AsmL. Such a semantics provides precise and non ambiguous definitions of AsmL. It is very useful to guarantee a unique implementation of the language and interpretation of its be-havior. Furthermore, they can be used in conducting formal proofs for sound abstractions or even to construct syntactical transformers to other languages. 1