Computer Science (31) This project pioneers an innovative methodology that increases the effectiveness of formal methods courses by providing students with sophisticated tools for understanding and proving program correctness. These tools are based upon Z, the common and powerful specification language and include type checking, specification animation and proof obligations. A separate tool is used for code generation. All of the tools provide research quality support to students learning to program in a formally correct manner.
Student performance is evaluated via tracking experimental and control groups through the core curriculum; the control group enrolls in similar courses but does not use the tools. We will measure and report two important factors: task completion time and error count.
