一句话：提出 Forge：基于 Alloy 的渐进式形式化方法教学工具与语言，支持可视化与测试。
形式化方法教学面临学生难以从编程过渡到形式建模、现有工具表达力跃迁过陡等问题。论文提出 Forge，一个基于 Alloy 语言与分析工具、并总结十余年 Alloy 教学经验改进而来的教学工具。Forge 提供表达能力逐步增强的语言序列，让学生渐进学习；支持输出结果的自定义可视化，使学生可借用领域特定表示；还提供多种测试功能以衔接编程与形式建模。作者阐述这些设计动机与方案，并基于多年课堂使用给出实质性评估。
This paper presents the design of Forge , a tool for teaching formal methods gradually. Forge is based on the widely-used Alloy language and analysis tool, but contains numerous improvements based on more than a decade of experience teaching Alloy to students. Although our focus has been on the classroom, many of the ideas in Forge likely also apply to training in industry. Forge offers a progression of languages that improve the learning experience by only gradually increasing in expressive power. Forge supports custom visualization of its outputs, enabling the use of widely-understood domain-specific representations. Finally, Forge provides a variety of testing features to ease the transition from programming to formal modeling. We present the motivation for and design of these aspects of Forge, and then provide a substantial evaluation based on multiple years of classroom use.
@article{paperbot2532,
title = {Forge: A Tool and Language for Teaching Formal Methods},
author = {Tim Nelson and Ben Greenman and Siddhartha Prasad and Tristan Dyer and Ethan Bove and Qianfan Chen and Charles Cutting and Thomas Del Vecchio and Sidney LeVine and Julianne Rudner and Ben Ryjikov and Alexander Varga and Andrew Wagner and Luke West and Shriram Krishnamurthi},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA1},
year = {2024},
doi = {10.1145/3649833}
}