Jovial Program Verifier Rugged Jovial Environment.
Abstract
This report summarizes project work carried out at the Computer Science Laboratory of SRI International under Contract F30602-78-C-0031 with Rome Air Development Center during the period November 1977 - November 1981. The project has been concerned with the development of a programming environment (Rugged Jovial Environment)--with verification tools as a principal component--for the specification, development, and formal verification of programs in JOVIAL-J73. The term verification here refers to proof of correctness with respect to formal specification by the method of Floyd assertions. The effort on this project has ranged from fairly abstract work on formal models of computation (in particular, regarding the semantics of JOVIAL constructs) to practical techniques for implementing these models. This has resulted in the development of a user-friendly system, written in INTERLISP, with the aid of which it is possible to verify JOVIAL software of significant complexity. In addition to our primary project work, we developed several very usefull software tools of more general applicability. These tools are also described in the report.
Document Details
- Document Type
- Technical Report
- Publication Date
- Oct 01, 1982
- Accession Number
- ADA123681
Entities
People
- Bernard Elspas
- David L. Snyder
- Dwight F. Hare
- Karl N. Levitt
Organizations
- SRI International