Formal methods for software correctness are critical to the future of software engineering - and so must be an essential part of software engineering education. Unfortunately, formal methods are often resisted by students due to perceived difficulty, mathematicity, and practical irrelevance. We redeveloped our software correctness course by taking a programming intensive approach, using the solver-aided language Dafny to provide instant formative feedback via automated assessment. Our redeveloped course increased student retention and resulted in the best evaluation for the course for at least ten years.
翻译:软件正确性的正式方法对于软件工程的未来至关重要,因此也必须是软件工程教育的重要组成部分。 不幸的是,正式方法常常由于人们所察觉的困难、数学性和实际无关紧要性而遭到学生的抵制。 我们重新开发了软件正确性课程,采用了编程强化方法,使用求解器辅助语言Dafny,通过自动评估提供即时形成反馈。 我们重新开发的课程增加了学生的留校率,并导致对课程进行至少十年的最佳评价。