Teaching Imperative Programming With Contracts at the Freshmen Level

We describe the experience with a freshmen-level course that teaches imperative programming and methods for ensuring the correctness of programs. Students learn the process and concepts needed to go from high-level descriptions of algorithms to correct imperative implementations, with specific applications to basic data structures and algorithms. A novel aspect of the course is that much of it is conducted in C0, a small safe subset of the C programming language, augmented with a layer of annotations to express contracts that are amenable to verification. The present version of the course assumes a basic understanding of programming (variables, expressions, loops, functions) and prepares students for subsequent computer systems courses taught in C as well as more advanced courses on algorithms and data structures