Penelope: An Ada Verification Environment, Developing Formally Verified Ada Programs. Volume 1
Abstract
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 (2,4). 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. Ada, Larch, Larch/Ada, Formal Methods, Formal Specification, Program Verification, Predicate Transformers, Ada Verification.
Document Details
- Document Type
- Technical Report
- Publication Date
- Nov 01, 1991
- Accession Number
- ADA249417
Entities
People
- Norman Ramsey