A Verification System for JOVIAL/J3 Programs (Rugged Programming Environment - RPE/1).
Final rept. 24 Sep 74-23 Oct 75,
STANFORD RESEARCH INST MENLO PARK CALIF
Pagination or Media Count:
This report describes a verification system for structured JOVIALJ3 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 Floyds 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 JOVIALJ3 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.
- Computer Programming and Software