Integrating Functional Program Verification Techniques to Computer Science Programs

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

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.