Developing formally verified Ada programs
Norman F. Ramsey · 1989
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 [1, 2]. 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 d...