Correctness and Incorrectness Reasoning with Types

Abstract:

Hoare-style program reasoning is a powerful mechanism for specifying programs' behaviours: with pre-/postcondition specifications, we can capture state changes in program executions. Types are equally fundamental to programming, yet the two typically remain separate issues. In this thesis, we bridge the gap between them, and show that the relationship runs in both directions. Hoare-style reasoning supplies the expressiveness that type systems lack, while type information supplies the precision that reasoning about errors lacks. We develop the two directions in turn, from the perspectives of correctness and incorrectness.

Hoare Logic was originally designed to guarantee program correctness, and proving type safety is essentially a kind of correctness reasoning. However, the relation between the two has not been systematically explored. Moreover, type systems—the classical framework for ensuring type safety—impose strong restrictions on types in order to eliminate type errors early, which causes problems for complex constructs and for dynamically typed languages. In the first part of the thesis, we discuss how type safety can benefit from Hoare Logic, demonstrating its advantages via path-sensitive types, flow-sensitive types, and comprehensive error handling. The resulting framework flexibly supports different paradigms, from statically typed languages (e.g., ML) with a rich set of types to dynamically typed languages (e.g., Python) with type mutation, via a novel concept called the separation type.

In the second part of the thesis, we show how incorrectness Hoare-style reasoning can benefit from types. Incorrectness Logic is a variant of Hoare Logic designed for proving the presence of errors: it retains the pre-/postcondition form but reverses its meaning. We extend Incorrectness Logic to Object-Oriented (OO) programming, and illustrate how to uphold the Liskov Substitution Principle, the essence of type inheritance, in this setting. We further tackle the challenge of reasoning about complex OO features, such as dynamic dispatching and method overriding, based on type information. Finally, we present a set of tools rooted in our logic; the experiments show that they outperform the state-of-the-art tools in detecting bugs in OO programs.

Taken together, the two parts tell a single story. Types and Hoare-style reasoning can be developed together, and each goes further in the other's company than it does alone.