Caos:一种可复用的操作语义Scala Web动画器(附实操教程扩展版)
Caos: A Reusable Scala Web Animator of Operational Semantics (Extended With Hands-On Tutorial)
AI总结:
本研究提出Caos框架,采用理论与工具同步构建的思路,借助Scala库生成交互式动画图以辅助形式化模型操作语义设计,可尽早发现理论缺陷,已在教学研究中成功应用于两种语言分析。
摘要:
本工具论文介绍了Caos:一种用于形式化模型结构化操作语义计算机辅助设计的方法论与编程框架。该框架包含一组Scala库以及一套工作流,可生成可视化交互式图表,对具有操作规则的给定抽象模型的结构与语义进行动画演示并提供分析视角。Caos采用理论基础与实用工具同步构建的思路,作为“基础优先设计(工具验证理论)”或“工具优先设计(基础验证实践)”的替代方案。Caos的优势在于,开发中的工具可立即用于自动运行大量规模可观的示例,从而尽早发现开发中的基础理论里的细微错误、意外结果与未预见的局限性。我们分享了Caos方法论与框架在自身教学和研究场景中的两个成功案例,分别分析了一种简单while语言和一种编排语言,包括它们的操作规则以及此类规则的并发组合。我们还进一步讨论了其他研究者如何将Caos集成到自己的分析工作与Scala工具中。
英文摘要:
This tool paper presents Caos: a methodology and a programming framework for computer-aided design of structural operational semantics for formal models. This framework includes a set of Scala libraries and a workflow to produce visual and interactive diagrams that animate and provide insights over the structure and the semantics of a given abstract model with operational rules. Caos follows an approach in which theoretical foundations and a practical tool are built together, as an alternative to foundations-first design ("tool justifies theory") or tool-first design ("foundations justify practice"). The advantage of Caos is that the tool-under-development can immediately be used to automatically run numerous and sizeable examples in order to identify subtle mistakes, unexpected outcomes, and unforeseen limitations in the foundations-under-development, as early as possible. We share two success stories of Caos' methodology and framework in our own teaching and research context, where we analyse a simple while-language and a choreographic language, including their operational rules and the concurrent composition of such rules. We further discuss how others can include Caos in their own analysis and Scala tools.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。