11-04

Proof Tools and Correct Program Development

A new approach to developing correct programs is proposed. The goal of the approach is to all developers to translate some of their intuitive ideas of why their code is correct into something machine checkable, like a proof fragment or partial proof. These partial proofs are to be integrated with the program text and checked at compile time.

As a modest step towards this goal, extended assertions are proposed. Extended assertions allow developers to say "If these assertions hold at these program points, then this other assertion holds at this program point." A simple implementation is demonstrated for a minimal imperative programming language without recursion or loops. Programs in this language together with their extended assertions are compiled into logical formulas, which can be checked automatically by the CVC (Coorperating Validity Checker") system. An overview of CVC follows. The talk concludes with a look at Rogue, which is an experimental programming language for manipulating expressions. The compiler from the recursion-free language to CVC's logic is written in Rogue, and Rogue is being considered for writing parts of CVC itself.