eCommons

 

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

Other Titles

Abstract

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.

Journal / Series

Volume & Issue

Description

Sponsorship

Date Issued

1981-09

Publisher

Cornell University

Keywords

computer science; technical report

Location

Effective Date

Expiration Date

Sector

Employer

Union

Union Local

NAICS

Number of Workers

Committee Chair

Committee Co-Chair

Committee Member

Degree Discipline

Degree Name

Degree Level

Related Version

Related DOI

Related To

Related Part

Based on Related Item

Has Other Format(s)

Part of Related Item

Related To

Related Publication(s)

Link(s) to Related Publication(s)

References

Link(s) to Reference(s)

Previously Published As

http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR81-467

Government Document

ISBN

ISMN

ISSN

Other Identifiers

Rights

Rights URI

Types

technical report

Accessibility Feature

Accessibility Hazard

Accessibility Summary

Link(s) to Catalog Record