Contracts and Correctness with JML
This course explores the powerful idea of using contracts, which are fundamentally assertion statements that can be ignored or checked at runtime, to document, test, and prove the correctness of programs. In particular, you will learn how to use the Java Modeling Language (JML) to help you write correct programs.
This course is based on my experience teaching the introductory data structures course at Carnegie Mellon. In that course, we used a language called C0 (pronounced "see naught"), which is a more limited form of the JML language. If you're not specifically interested in Java, the course on Getting it Right is probably a better fit.
This course expects some familiarity with imperative programming with loops and recursive procedures. Additionally, you should either have written some Java or have some understanding of objects and be comfortable picking up new languages.
During this course, you will:
- Use Java Modeling Language (JML) to document preconditions and postconditions and (optionally) enforce them at runtime.
- Write and debug internal contracts (loop invariants and data structure invariants) that can be checked at runtime.
- Experience the power of combining unit tests and internal contracts for debugging code.
- Explain when contracts do or do not suffice to prove the safety and correctness of code.
- Prove (on paper) the correctness of loops, recursive programs, and somewhat complex data structures using contracts.
- Take a look at advanced tools that allow these proofs to be checked by a computer.
Start writing Java programs that are less wrong today!