A bitvectors library for PVS /

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...

Full description

Bibliographic Details

Main Author:	Butler, Ricky W. (Author)
Format:	Government Document eBook
Language:	English
Published:	Washington, D.C. : National Aeronautics and Space Administration, 1996.
Series:	NASA technical memorandum ; 110274.
Subjects:	Hardware. Proving. Bit synchronization. Integers. Libraries.
Online Access:	https://purl.fdlp.gov/GPO/gpo75879