Laboratories in a Formal Methods-and OOP-Oriented Approach to the Early Computer Science Curriculum

面向对象程序设计（OOP）已经获得了广泛的接受，并且在一些机构的较早阶段就开始教授。在入门级使用形式化方法（FM）是不寻常的，但它的使用已经被证明对学生在第一个计算机科学（CS）课程中有具体的好处。这个项目的目标是将OOP和FM集成到早期的CS序列中，从而导致大二的课程将OOP和FM结合到面向对象设计的介绍中。这门课程成为之前课程的顶点，也是之后课程的门户。实现这一目标的计划是建立在Troeger使用FM教授第一门CS课程的成功基础上，以及在这里和其他地方在第二门课程中使用OOP的成功。这将在第二门课程（传统上称为数据结构）中产生FM和OOP的混合。当然，这种混合将是初级的，但却是真实的。然后在顶点/门户课程中，作为这些思想的延续，引入了面向对象设计，将其应用于更大更现实的问题，并引入了更多的面向对象方法。这个项目的目标受众是每所教授计算机科学的学校。这个项目预计将对计算机科学的教学方式产生重大影响。该部门计划通过讲习班、论文和演讲以及两本已签订合同的教科书来传播成果。

Object-Oriented Programming (OOP) has gained wide acceptance and is being taught at a relatively early level at some institutions. The use of Formal Methods (FM) at the introductory level is unusual, but its use has been demonstrated to have concrete benefits for students in the first computer science (CS) course. The objective of this project is to integrate OOP and FM into an early CS sequence, leading to a sophomore course in which OOP and FM are combined in an introduction to object-oriented design. This course becomes a capstone of what precedes it and a gateway to what follows. The plan to accomplish this goal is to build on Troeger's demonstrated success in teaching the first CS course using FM, and the success demonstrated here and elsewhere in using OOP in the second course. This will yield a blend of FM and OOP in the second course, traditionally called Data Structures. The blend will be at an elementary level, of course, but real. Then in the capstone/gateway course, object-oriented design is introduced as a continuation of these ideas, applied to larger and more realistic problems and with more of the OOP methodology brought in. The intended audience for this project is every school teaching computer science. This project is expected to have a major impact on how CS is taught. The department is planning to disseminate results through workshops, papers and presentations, and two textbooks for which it already has contracts.