Staged Program Development

Abstract

A major issue facing software development and maintenance is the sheer complexity of programs. Even software designs that start off simple often evolve into programs that are both brittle and hard to understand.

In this talk, I advocate programming in stages, where the programming language allows the program design to be described at varying levels of abstraction. Higher levels of abstraction focus on the intent of the design, whereas lower levels of abstraction introduce optimizations and other details. Since the layering is expressed in the programming language, the stages are preserved as part of the program text. Therefore, the stages help break down the program's complexity not only during development but also during maintenance.

I will describe some language features, both old and new, that encourage staged development. To help communicate the vision, I will demonstrate Dafny, a research programming system whose language blends specifications, imperative programming, and staged program refinements and whose development environment is powered by an automatic program verifier that constantly analyzes the program to help the programmer get details right.

Joint work with Jason Koenig.

Biographical Sketch

K. Rustan M. Leino is a Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research. He is known for his work on programming methods and program verification tools.

At Microsoft Research, he has led the Spec# project, which brings enforced pre- and post-conditions to the .NET platform. He is the architect of the Boogie program verification framework, which underlies many program verifiers, including ones for C and Eiffel. A more recent research focus is the language and state-of-the-art verifier Dafny. With Dafny, Leino's mission is not just to provide a tool that helps teach programmers to reason about programs, but also to provide a vision for the kind of automatic reasoning support that all future programming environments may provide. Previously, at DEC/Compaq SRC, Leino led the ESC/Java project and worked on specifications on the pioneering ESC/Modula-3 project.

Before getting his Ph.D. at Caltech in 1995, Leino wrote and designed object-oriented software as a technical lead in the Windows NT group at Microsoft. Leino collects thinking puzzles on a popular web page and hosts the Verification Corner video show on channel9.msdn.com. In his spare time, he plays music and, recently having ended his tenure as cardio exercise class instructor, is trying to learn to dance.