Developing Formally Verified Ada Programs (Abstract)

Norman Ramsey

Odyssey Research Associates has undertaken a study of the feasibility of developing formally verified Ada programs. We have designed a specification language for sequential Ada programs. It is a member of the Larch family of specification languages. We have built a prototype program editor that is intended to help programmers develop programs and proofs from specifications, as advocated by Dijkstra and Gries. It contains predicate transformers, which compute wp (an approximation to the weakest precondition of a program), and it generates verification conditions.

The semantics of the specification language and the definition of the predicate transformers are derivable from a denotational definition of sequential Ada. The predicate transformers can be proved sound with respect to these definitions by structural induction on programs. The denotational-style definition of the predicate transformers is well suited to an implementation as an attribute grammar.

The program editor is designed to be used on program fragments, not just complete programs. The next step in improving the prototype editor is to find ways to simplify the intermediate values of wp so they can be used to guide the development of fragments into programs.

The full paper is available in PostScript form.