CSE 331: Software Design & Implementation

CSE 331: Topics

The course is organized into 10 topics. We plan to cover one topic per week.

1. Specifications & Testing

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.

2. Reasoning About Functional Code

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.

3. Specifications of Immutable ADTs

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.

  • Lecture slides
  • Section slides and worksheet
  • At-home worksheet (only tasks 1–3 are required). Change log:
    • Added the AF and clarified the instructions for Task 1

4. Reasoning with Variable Mutation

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.

  • Lecture slides
  • Section slides and worksheet
  • At-home worksheet (only tasks 1–3 are required). Change log:
    • Updated Task 1(b) to also allow one step forward before reasoning backward.
    • The invariants of both loops were updated in Task 4

5. Specifications of Mutable ADTs

In this topic, we revisit ADTs but now consider methods that mutate their arguments or their own state. This requires changes to how ADT specifications are written. More importantly, it introduces the potential for interdependencies between classes that make them more difficult to change and understand and can lead to very painful bugs. We will discuss some best practices for avoiding those problems.

  • Lecture slides
  • Section slides and worksheet
  • At-home worksheet (only tasks 1–3 are required). Change log:
    • The example given in Task 2(b) has been fixed. It was originally reading the list in the wrong direction when calculating max.
    • The definition of helper2 has been fixed. It originally had helper1 and helper2 swapped in the second case of the definition and had an unnecessary list reversal.

6. Reasoning About ADTs

In this topic, we will see how we can put together specifications of ADTs with our correctness tools for functions in order to check the correctness of each method in an ADT implementation (assuming that we do not allow any representation exposure!).

  • Lecture slides
  • Section slides and worksheet
  • At-home worksheet (only tasks 1–3 are required). Change log:
    • Task 1 code was updated to fix a bug. (This has no impact on the actual questions.)
    • Task 3(b) instructions removed confusing reference to "n" (which conflicted with the "n" in the code).
    • Task 3(c) fixed the definition of Q in the code.

7. Making Bugs Impossible

In this topic, we will look at ways to make bugs impossible by having the type checker prevent them. We will start by looking at ways to do this within the Java type system. Then, we will look at the type systems of other languages — Python, TypeScript, and Rust — that have different mechanisms of preventing important types of bugs.

  • Lecture slides
  • Section slides and worksheet
  • At-home worksheet (only tasks 1–3 are required). Change log:
    • Fixed a bug in the Rust code for Task 1(b). Was missing an "&mut" in the call to f2.

8. Reasoning About Array Indexing

In this topic, we will look at how to reason about code with array indexing. As we will see, this creates potential bugs that cannot occur with lists. Array indexing gives us extra power but comes at a cost of more complex reasoning, requiring the use of prefixes, suffix, and “for any” facts to describe their states.

9. Type Polymorphism

In this topic, we will look at ways that we can write code that can be used for types without any changes. The first way is through the use of subtypes. The second way is through the use of type parameters, which are called “generics” in Java.

10. More Loop Reasoning

In this topic, we will look at some more advanced topics related to loops. First, we will see how to cope with some complicated, “for any” facts that appear in loop invariants. Second, we will explore the relationship between loops and recursion in more detail.

That's all, folks!