Accession Number:

ADA024395

Title:

A Verification System for JOVIAL/J3 Programs (Rugged Programming Environment - RPE/1).

Descriptive Note:

Final rept. 24 Sep 74-23 Oct 75,

Corporate Author:

STANFORD RESEARCH INST MENLO PARK CALIF

Report Date:

1976-03-01

Pagination or Media Count:

121.0

Abstract:

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.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE