NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
HDM/PASCAL Verification System User's ManualThe HDM/Pascal verification system is a tool for proving the correctness of programs written in PASCAL and specified in the Hierarchical Development Methodology (HDM). This document assumes an understanding of PASCAL, HDM, program verification, and the STP system. The steps toward verification which this tool provides are parsing programs and specifications, checking the static semantics, and generating verification conditions. Some support functions are provided such as maintaining a data base, status management, and editing. The system runs under the TOPS-20 and TENEX operating systems and is written in INTERLISP. However, no knowledge is assumed of these operating systems or of INTERLISP. The system requires three executable files, HDMVCG, PARSE, and STP. Optionally, the editor EMACS should be on the system in order for the editor to work. The file HDMVCG is invoked to run the system. The files PARSE and STP are used as lower forks to perform the functions of parsing and proving.
Document ID
19840017247
Document Type
Other
Authors
Hare, D. (SRI International Corp. Menlo Park, CA, United States)
Date Acquired
August 12, 2013
Publication Date
August 1, 1983
Publication Information
Publication: Invest., Develop., and Evaluation of Performance Proving for Fault-Tolerant Computers
Subject Category
COMPUTER PROGRAMMING AND SOFTWARE
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.

Related Records

IDRelationTitle19840017239Analytic PrimaryInvestigation, Development, and Evaluation of Performance Proving for Fault-tolerant Computers
Document Inquiry