Proving Programs Correct Using Java Types
Formal tools for constructing proofs of correctness of programs have a long history of development in research labs, but have typically not been widely deployed in software development tools. In this talk, I'll demonstrate that the off-the-shelf Java type system is sufficiently powerful to encode non-trivial proofs of correctness. We use an encoding of propositional logic into Java types, based on a first-order fragment of Logical Frameworks. Using this encoding, we can provide methods with Hoare preconditions and postconditions, which are validated by the Java typechecker. As motivating examples, we consider the monotone typestates system of F\"ahndrich and Leino, and the closely related object initialization system of Myers and Qi. We show how their examples can be proved correct in the Java typechecker, and extend their examples with a proof of correctness of a one-pass cyclic graph construction algorithm, which improves F\"ahndrich and Leino's 2-pass algorithm.