一句话：报告以软件规约为中心的一年级课程经验，创建支持契约与性质测试的教学语言，并用学生访谈评估效果。
本文是一篇教学经验报告，主张软件规约应在本科课程中占据显著位置。作者描述了一门将软件规约置于核心的一年级课程，并为此创建了一门教学编程语言，重点支持契约和基于性质的测试。课程作业取材于不同领域的真实程序，旨在展示形式规约如何提升对代码正确性的信心。作者通过学生访谈评估教学效果，结果表明该方法能有效帮助学生理解形式规约与软件构建之间的相关性。
A course on software specification deserves a prominent place in the undergraduate curriculum. This report describes our experience teaching a first-year course that places software specification front and center. In support of the course, we created a pedagogic programming language with a focus on contracts and propertybased testing. Assignments draw on real-world programs, from a variety of domains, that are intended to show how formal specification can increase confidence in the correctness of code. Interviews with students suggest that this approach successfully conveys how formal specification is relevant to software construction.