锻造：教授形式方法的工具

发布于 7 月 27 日

Course Introduction: For the past decade, they've been studying how to get students into formal methods. Focus is on the "other 90%" not naturally inclined. Course Logic for Systems infuses FM thinking into system-building students.
Course Focus: The bulk of the course focuses on solver-based formal methods, starting with Alloy. Alloy has benefits like feeling like a programming language, running code like an IDE, used for verification and state-exploration, with a nice visualizer and allows lightweight exploration with refinement.
Issues with Alloy and Forge: Over the years, they faced various issues with Alloy. In response, they built a new FM tool called Forge with three features:
- Layers Alloy into a series of language levels instead of full complexity.
- Uses the Sterling visualizer by default (a better version of Alloy's), and it allows custom visualizations for domain-specific needs. The default visualization can be unhelpful, while custom visualization fixes this.
- Explores [property-based testing] as a way to get students from programming to FM and provides preliminary answers in Forge.
Example Visualizations: Shows an example of default Sterling output and custom visualization output to illustrate the difference.
More Details and Tryout: For more details, see the paper. And encourage to try out Forge.
Acknowledgements: Grateful for support from the U.S. National Science Foundation (award #2208731).

阅读 10