A Verification System for JOCIT/J3 Programs (Rugged Programming Environment - RPE/2)

Abstract

This report describes work done during the second year of a research and development program aimed ultimately at a Rugged Programming Environment for JOVIAL. The RPE/1 verification system designed and built during the first year has been greatly extended and improved in several ways. The basic method of verification remains the same--that of inductive assertions. The input processor has been modified to handle virtually of all JOCIT instead of the small subset covered by the RPE/1 system. The overall speed of verification has been increased by a factor of over 25. Ease of user interaction with the system has been greatly enhanced by adding facilities for carrying out and saving partial proofs of programs, for extending the assertion language, and for enabling top- down and bottom-up proofs for well-structured programs. Moreover, the entire system has been translated into MACLISP, the system files have been transferred to the RADC-MULTICS Honeywell 6180 computer, and a sample verification (shown in the report) has been carried out entirely on the RADC computer.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jul 01, 1977
Accession Number
ADA042670

Entities

People

  • B. Elspas
  • J. M. Spitzen
  • R. E. Shostak

Organizations

  • SRI International

Tags

Communities of Interest

  • C4I
  • Energy and Power Technologies
  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Air Force
  • Algorithms
  • Arithmetic
  • Automatic
  • Compilers
  • Computer Programming
  • Computer Programs
  • Computers
  • Construction
  • Equations
  • Grammars
  • Identities
  • Integer Programming
  • Language
  • Numbers
  • Standards

Fields of Study

  • Computer science

Readers

  • Artificial Intelligence
  • Computer Engineering
  • Computer Science.