AsmL Semantics in Fixpoint

AsmL is a novel executable specification language based on the theory of State Machines (ASMs). It represents one of the most powerful practical engines to write and execute ASMs. In this report, 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 behavior. Furthermore, they can be conducting formal proofs for sound abstractions or even to construct syntactical transformers to other languages. 1 

• Type: Conference
• Year: 2005
• Where: ASM
• Authors: Ali Habibi, Sofiène Tahar
• Keywords: ASM 2005, Executable Specification Language, Microbiology, Powerful Practical Engines, Trace-based Operational Semantics