Maintaining Database Integrity with Refinement Types

Given recent advances in automated theorem proving, we present a new method for determining whether database transactions preserve integrity constraints. The constraints we consider are check constraints and referential-integrity constraints—extracted from SQL table declarations—and application-level invariants expressed as formulas of first-order logic. Our motivation is to use static analysis of database transactions as an alternative to costly runtime integrity checks. We work in the setting of a functional multi-tier language, where functional code is compiled to SQL in order to query and update a relational database. We use refinement types (types qualified by logical formulas) to track constraints on data and the underlying state of the database; our static analysis of transactional code uses a refinement-type checker, which relies on recent highly efficient SMT algorithms to check proof obligations. Our method is based on a list-processing semantics for an SQL fragment within the functional language, and is illustrated by a series of programming examples. Our analysis could be applied either at the time of code development, to catch bugs early, or later at the time of deployment on the database server, to allow only integrity-preserving stored procedures to be accepted.