AVID: A system for the Interactive Development of Verifiably Correct Programs

The AVID system is designed to Aid Verification through the techniques of Interactive program Development. AVID continues the work in programming logics begun at Cornell University in 1975. It provides a syntax-directed editing environment for the development by stepwise refinement of programs and proofs in the PL/CV2 programming logic. AVID is another step in the continuing effort to provide methods and software tools for developing correct programs. AVID contains a number of important contributions to the area of program/proof development. To allow the full power of the AVID verification facilities to be applied to programs developed by stepwise refinement, we created a new program construct, called an ATTAIN block, that formalizes the concept of a refinement level. This construct allows the independent verification of different refinement levels, and thus of partially developed programs. Using this construct, AVID can guarantee that the refinement in a top-down development actually implements its high-level specification. AVID is the first system to support the interactive display of logical dependency in proofs. We have developed a new algorithm, built on the congruence closure method for deciding the theory of equality, that efficiently determines logical dependency within this theory. This algorithm is independent of the AVID system, and has potential applications wherever the congruence closure method is used. AVID also contains some significant contributions to the area of syntax-directed editor design. AVID makes use of a standard, powerful, and widely available screen-oriented editor as its user interface. The system design gives a strategy for the incorporation of other powerful editors into syntax-directed development systems. AVID is also the first system to make extensive use of derived nonterminals to avoid redundant specification and to guide the user in developing his proof. Perhaps AVID's most important contribution is its demonstration of the feasibility of a system to support and enforce the development by stepwise refinement of provably correct programs. For programs that must be correct, this approach may be one of the most promising. One final contribution of the AVID project is the system itself as a base for future research. The modular design of the AVID system and its facilities for the high-level description of AVID language constructs make the system easy to modify and to build on. There are already several projects planning to use AVID in this fashion. AVID has been implemented on a DEC VAX 11/780 under the Berkeley UNIX operating system. The current version of the system, which supports the development and verification of the predicate calculus portion of PL/CV2, consists of approximately 20,000 lines of C language source code. When running on the VAX, the current system requires 230K bytes of memory. A version of the system suitable for distribution is expected to be available by January 1982