A JOVIAL Verifier.
Abstract
This Interim Report describes progress during the first year of research and development on a program verification system supporting the design, development, and formal verification of programs written in JOVIAL-J73-I. The work reported here represents an outgrowth and continuation of earlier efforts concerned with JOVIAL-J3 (JOCIT version). Detailed descriptions are presented of progress and future plans in the following areas: (a) Analysis of the JOVIAL-J73/I language with respect to verifiability, leading to formal definitions of its syntax and semantics, and to the enhancement of the language by assertion constructs for the purposes of specification and verification (b) The organization, technical development, and implementation of portions of the JOVIAL Verifier - in particular, of a verification condition generator and deductive subsystems; (c) The selection, analysis, and verification of two real software systems of significant size and complexity, critical parts of which will be implemented in J73/I and which is hoped to be verified by means of the JOVIAL Verifier. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Jul 01, 1979
- Accession Number
- ADA075108
Entities
People
- B. Elspas
- M. S. Moriconi
- M. W. Green
- R. E. Shostak
Organizations
- SRI International