Rule formats can quickly establish meta-theoretic properties of process algebras. It is then desirable to identify domain-specific languages (DSLs) that can easily express rule formats. In prior work, we have developed Lang-n-Change, a DSL that includes convenient features for browsing language definitions and retrieving information from them. In this paper, we use Lang-n-Change to write a validator for the GSOS rule format, and we augment Lang-n-Change with suitable macros on our way to do so. Our GSOS validator is concise, and amounts to a few lines of code. We have used it to validate several concurrency operators as adhering to the GSOS format. Moreover, our code expresses the restrictions of the format declaratively.
翻译:规则格式能够快速确立进程代数的元理论性质。因此,识别出易于表达规则格式的领域特定语言(DSL)具有重要意义。在前期工作中,我们开发了Lang-n-Change这一DSL,其包含便于浏览语言定义及从中检索信息的实用特性。本文利用Lang-n-Change为GSOS规则格式编写验证器,并在实现过程中为其添加了适当的宏功能。我们的GSOS验证器代码简洁,仅需数行即可完成。通过该验证器,我们已成功验证多个并发算子符合GSOS格式规范。此外,我们的代码以声明式方式表达了格式约束条件。