The main focus of the class is teaching imperative programming and methods to
prove the correctness of code. It introduces searching and sorting algorithms as well
as data structures like linked lists, stacks, queues, heaps, trees, tries, etc.
The first part of the course is taught in
C0,
which is a small and safe subset of C,
augmented with contracts, and specically developed for teaching this course.
Shortly after mid-semester, students are introduced
to C, and concepts like memory management, generic data types and function pointers are
discussed, along with various quirks of C. The course culminates with the students writing
a virtual machine for C0 in C, that is able to execute byte code generated by the C0 compiler.