A Verification System for JOVIAL/J3 Programs (Rugged Programming Environment - RPE/1).
Abstract
This report describes a verification system for structured JOVIAL/J3 programs that was designed and implemented during the first year of a research and development program aimed ultimately at a 'Rugged Programming Environment' for JOVIAL. The verification system uses Floyd's method of inductive assertions, and includes a syntax transducer, verification condition generator, and a semiautomatic deductive system for proving the verification conditions. Other work performed on the project included the design of an assertion language for the specification of JOVIAL/J3 programs, and the elaboration of a methodology for carrying out hierarchical verification of suitably structure programs. The report contains sample output illustrating the verification of simple J3 programs.
Document Details
- Document Type
- Technical Report
- Publication Date
- Mar 01, 1976
- Accession Number
- ADA024395
Entities
People
- B. Elspas
- J. M. Spitzen
- R. E. Shostak
- R. S. Boyer
Organizations
- SRI International