NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Proving the correctness of a flight-director program for an airborne minicomputerProgram verification procedures are described and used to determine the correctness of a program written for an airborne computer. The basic method relies on the inductive assertion method of Floyd (1967), modified and extended for application to a machine-language situation. Correctness considerations in the flight director program include self-modification, system correctness, executable instructions, overflow, approximate calculations with fractional quantities, and fixed point scaling. An example proof of correctness, which proceeds by proving the correctness of a certain subroutine, is provided.
Document ID
19770068409
Acquisition Source
Legacy CDMS
Document Type
Reprint (Version printed in journal)
Authors
Maurer, W. D.
(George Washington University Washington, D.C., United States)
Date Acquired
August 9, 2013
Publication Date
April 1, 1977
Subject Category
Computer Programming And Software
Accession Number
77A51261
Funding Number(s)
CONTRACT_GRANT: NSF DCR-73-03431-A01
CONTRACT_GRANT: NSG-1170
Distribution Limits
Public
Copyright
Other

Available Downloads

There are no available downloads for this record.
No Preview Available