AsmL Semantics in Fixpoint
AsmL Semantics in Fixpoint
复制标题
Fixpoint 中的 AsmL 语义
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
S. Tahar
中科院分区：
文献类型：
--
作者：
A. Habibi;S. Tahar
ASML是一种基于抽象状态机(ASM)理论的新型可执行规范语言。它代表了编写和执行ASM最强大的实用引擎之一。本文对ASML的主要部分提出了一种完整的基于小步轨迹的操作语义。这样的语义为ASML提供了精确且明确的定义。它们对于保证语言的唯一实现和对其行为的解释非常有用。此外，它们还可用于对声音抽象进行形式化证明，甚至用于构造到其他语言的句法转换器。
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 paper, 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. They are very useful to guarantee a unique implementation of the language and interpretation of its behavior. Furthermore, they can be used in conducting formal proofs for sound abstractions or even to construct syntactical transformers to other languages.