A bitvectors library for PVS / Ricky W. Butler [and four others].

Author/creator Butler, Ricky W. author.
Other author Langley Research Center, issuing body.
Format Electronic
Publication InfoWashington, D.C. : National Aeronautics and Space Administration, 1996.
PublicationHampton, Virginia : National Aeronautics and Space Administration, Langley Research Center, August 1996.
Description1 online resource (17 pages) : illustrations.
Supplemental Contenthttps://purl.fdlp.gov/GPO/gpo75879

SeriesNASA technical memorandum ; 110274
NASA technical memorandum 110274. ^A467613
Abstract This 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.
General note"August 1996."
General note"Performing organization: National Aeronautics and Space Administration Langley Research Center"--Report documentation page.
General noteCRDP Project record.
Bibliography noteIncludes bibliographical references (pages 16-17).
Report noteTechnical memorandum.
Funding informationSponsored by the National Aeronautics and Space Administration WU 505-64-10-13
Source of descriptionDescription based on online resource; title from PDF title page (NASA, viewed Dec. 23, 2016).
Source of descriptionPrint version record.
Issued in other formPrint version: Bitvectors library for PVS
Issued in other formMicrofiche version: Bitvectors library for PVS
GPO item number0830-D (online)
Govt. docs number NAS 1.15:110274

Availability

Library Location Call Number Status Item Actions
Electronic Resources Access Content Online ✔ Available