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.