The course is organized into 10 topics. We plan to cover one topic per week.
Even when we are asking AI to write code for us, since AI cannot read our minds, it is important to be able to write a clear specification, stating in precise terms what that code needs to do. In this topic, we will look at how specifications for methods are written in Java and in formal mathematics.
We will also discuss how to get some confidence (though not complete confidence) that the specification is correct by checking it on a well-designed set of test cases.
Next, we turn to implementing the specifications we saw in Topic 1. The most important property of any implementation is correctness. While testing is helpful for ensuring correctness, the only way to guarantee the code is correct is to prove it.
In this topic, will see how to reason formally and prove the correctness of code that does not involve any mutation. Code with mutation is harder to reason about and will be examined in future topics.
In this topic, we will look at how to create abstractions that hide the details of data structures rather than code, in the form of an abstract data type (ADT). We will see how to write a precise specification both for the client-facing operations of the ADT and the implementer-facing choice of data structures.
In this topic, we continue our study of reasoning, now moving to slightly more complex (and more common) types of code. Previously we considered code without mutation, in which complex calculations are performed via recursion. Here, we will look at code that mutates local variables. In particular, this allows us to write loops instead of recursion. However, it also makes reasoning more complicated, necessitating new reasoning tools.