一句话：介绍教育游戏 FormalZ，以深度游戏化方式帮助学生学习书写前后条件形式规约。
为软件提供形式规约有很多好处，但形式方法课程常被学生认为枯燥，教学并不容易。本文提出一款名为 FormalZ 的游戏，供教师在课堂中引入变化。学生通过玩游戏获得乐趣，同时学习以 pre- and post-conditions 形式书写形式规约的基础。与 Pex、Code Defenders 等软件工程主题的教育游戏不同，FormalZ 采用深度游戏化（deep gamification）方法，让游戏玩法占据更核心的位置，以产生更强的参与感。本文是一篇工作进展短文，介绍了 FormalZ 的首个实现及其初步用户评估结果。该实现在功能上完整并经过测试，但用户界面的打磨仍是未来工作。
There are many benefits in providing formal specifications for our software. However, teaching students to do this is not always easy as courses on formal methods are often experienced as dry by students. This paper presents a game called FormalZ that teachers can use to introduce some variation in their class. Students can have some fun in playing the game and, while doing so, also learn the basics of writing formal specifications in the form of pre-and post-conditions. Unlike existing software engineering themed education games such as Pex and Code Defenders, FormalZ takes the deep gamification approach where playing gets a more central role in order to generate more engagement. This short paper presents our work in progress: the first implementation of FormalZ along with the result of a preliminary users' evaluation. This implementation is functionally complete and tested, but the polishing of its user interface is still future work.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{abs-1903-00334,
title = {Having Fun in Learning Formal Specifications},
author = {Wishnu Prasetya and Craig Leek and Orestis Melkonian and Joris ten Tusscher and Jan van Bergen and Jasper Everink and Thomas van der Klis and Rick Meijerink and Roan Oosenbrug and Jelle Oostveen and Tijmen van den Pol and Wink van Zon},
booktitle = {ICSE},
year = {2019},
doi = {10.1109/icse-seet.2019.00028}
}