NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Collections About News Help Login
Back to Results
A Bitvectors Library for PVSThis paper describes a bitvectors library that has been developed for PVS. The library defines a bitvector as a function from a subrange of the integers into (0,1). The library provides functions that interpret a bitvector as a natural number, as a 2's complement number, as a vector of logical values and as a 2's complement fraction. The library provides a concatenation operator and an extractor. Shift, extend and rotate operations are also, defined. Fundamental properties of each of these operations have been proved in PVS.
Document ID
19970001377
Acquisition Source
Legacy CDMS
Document Type
Technical Memorandum (TM)
Authors
Butler, Ricky W. (NASA Hampton, VA United States)
Miner, Paul S. (NASA Hampton, VA United States)
Srivas, Mandayam K. (SRI International Corp. Menlo Park, CA United States)
Greve, Dave A. (Rockwell International Corp. Cedar Rapids, IA United States)
Miller, Steven P. (Rockwell International Corp. Cedar Rapids, IA United States)
Date Acquired
September 6, 2013
Publication Date
August 1, 1996
Subject Category
Computer Systems
Report/Patent Number
NAS 1.15:110274
NASA-TM-110274
Accession Number
97N11194
Funding Number(s)
PROJECT: RTOP 505-64-10-13
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.

Related Records

There are no records associated with this record.
No Preview Available