Engaging Students in Specification and Reasoning: 'Hands-On' Experimentation and Evaluation

摘要

We introduce a "hands-on" experimentation approach for teaching mathematical specification and reasoning principles in a software engineering course. The approach is made possible by computer-aided analysis and reasoning tools that help achieve three central software engineering learning outcomes: (ⅰ) Learning to read specifications by creating test points using only specifications; (ⅱ) Learning to use formal specifications in team software development while developing participating components independently; and (ⅲ) Learning the connections between software and mathematical analysis by proving verification conditions that establish correctness for software components. Experimentation and evaluation results from two institutions show that our approach has had a positive impact.