© 2021 Strange Loop
Contracts are a three-decade-old idea whose time stubbornly refuses to have come. Contracts allow preconditions, postconditions, and internal invariants of functions and objects to be written out as code, presented as documentation, checked while the program is running, and used to reason about programs. Contracts are complementary to types, and can easily express complicated conditions (these two inputs have to be mutually prime, the function will return an array that's twice as long). If you've programmed with dependent types, contracts feel like unit testing. If you've written a lot of unit tests, contracts will feel like an amazing new type system. If the previous two sentences are terrifying, then that's terrific too: contracts are a great way of learning how to write imperative and object-oriented programs correctly. (They're also great for learning how to write functional programs, but I'll only talk about that a little bit.)
This talk will show off the Java Modelling Language (JML), an industrial-strength contract language bolted onto the head of Java, and C0, a simplified version of JML developed for Carnegie Mellon University's introductory data structures course. I'll talk about how contracts can be used to teach introductory computer science students (AND YOU) how to write correct algorithms and better tests. We'll also take a quick look at how JML was used with a computer-assisted theorem prover to diagnose and fix a bug in java.utils.Collection.sort()!
Rob Simmons is a native Atlanta, Georgian and hopeless cat lover. He finished his Ph.D. in computer science from Carnegie Mellon University in 2012. After that, he taught computer science at Carnegie Mellon University's Computer Science Department from 2012-2016. In mid-2016, he moved to Raleigh, North Carolina where his wife, Chris Martens, is a professor of computer science at North Carolina State University. He currently does freelance computer science education, tutoring, and curriculum development.