Programming with Specifications

This thesis explores the use of specifications for the construction of correct programs. We go beyond their standard use as run-time assertions, and present algorithms, techniques and implementations for the tasks of 1) program verification, 2) declarative programming and 3) software synthesis. These results are made possible by our advances in the domains of decision procedure design and implementation. In the first part of this thesis, we present a decidability result for a class of logics that support user-defined recursive function definitions. Constraints in this class can encode expressive properties of recursive data structures, such as sortedness of a list, or balancing of a search tree. As a result, complex verification conditions can be stated concisely and solved entirely automatically. We also present a new decision procedure for a logic to reason about sets and constraints over their cardinalities. The key insight lies in a technique to decompose con- straints according to mutual dependencies. Compared to previous techniques, our algorithm brings significant improvements in running times, and for the first time integrates reasoning about cardinalities within the popular DPLL(T ) setting. We integrated our algorithmic ad- vances into Leon, a static analyzer for functional programs. Leon can reason about constraints involving arbitrary recursive function definitions, and has the desirable theoretical property that it will always find counter-examples to assertions that do not hold. We illustrate the flexibility and efficiency of Leon through experimental evaluation, where we used it to prove detailed correctness properties of data structure implementations. We then illustrate how program specifications can be used as a high-level programming construct ; we present Kaplan, an extension of Scala with first-class logical constraints. Kaplan allows programmers to create, manipulate and combine constraints as they would any other data structure. Our implementation of Kaplan illustrates how declarative programming can be incorporated into an existing mainstream programming language. Moreover, we examine techniques to transform, at compile-time, program specifications into efficient executable code. This approach of software synthesis combines the correctness benefits of declarative programming with the efficiency of imperative or functional programming.