Integrating Functional Program Verification Techniques to Computer Science Programs

本项目的基本目标是通过提高计算机科学专业本科生对计算机程序正确性的推理能力，提高软件开发人员创建和验证可靠软件的能力。为了达到这个目标，这个项目有一个技术目标和两个教育目标。技术研究的目的是开发适用于本科计算机科学课程教学的实用验证技术。教育研究目标是开发和传播程序验证的学习模块和材料，并将正式的程序验证-基于数学的推理-整合到计算机科学与工程本科课程中。通过集合和函数的运用，实现了将程序验证融入本科课程的数学教学目标。结合规范语言的最新进展，开发了一种注释符号，将程序作为从输入值到输出值的函数进行记录。注释符号支持从非正式到完全数学的一系列形式，以帮助逐步整合到课程中。支持自然、直观、正向推理的功能验证方法被扩展为面向对象程序的模块化验证，并且开发了用于教授和学习功能规范和验证的轻量级工具。通过首先提供关于程序验证的实验课程，然后以此经验为指导，在整个本科课程中引入基于问题的学习模块，可以实现课程的增量整合。该方法通过将模块整合到从入门课程到高级顶点课程的本科计算机科学课程中来证明。

Computer Science (31)The fundamental goal of this project is to raise the competence of software developers to create and verify reliable software by improving the ability of undergraduate computer science students in reasoning about the correctness of computer programs. To reach this goal, this project has one technical objective and two educational objectives. The technical research objective is to develop practical verification techniques suitable for teaching in undergraduate computer science courses. The educational research objectives are to develop and disseminate learning modules and materials on program verification and to integrate formal program verification - reasoning based on mathematics - into the undergraduate computer science and engineering curriculum.The mathematics to achieve this project's educational goals of integrating program verification into the undergraduate curriculum is through the use of sets and functions. An annotation notation incorporating recent advances in specification languages is developed to document programs as functions from input values to output values. The annotation notation supports a spectrum of formality, from informal to fully mathematical, to assist an incremental integration into the curriculum. A functional verification approach, which supports a natural, intuitive, forward reasoning, is extended for modular verification of object-oriented programs, and lightweight tools are developed for teaching and learning functional specification and verification. An incremental integration to the curriculum is achieved by first delivering an experimental course on program verification and then, using this experience as a guide, introducing problem-based learning modules throughout undergraduate courses. The approach is demonstrated by integrating modules into the undergraduate computer science curriculum from the introductory courses to the senior capstone course.