Proof Tools and Correct Program Development
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.