The Resource A bitvectors library for PVS, Ricky W. Butler [and four others]

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

Label
A bitvectors library for PVS
Title
A bitvectors library for PVS
Statement of responsibility
Ricky W. Butler [and four others]
Creator
Contributor
Author
Issuing body
Subject
Language
eng
Summary
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
Member of
Cataloging source
OCLCE
http://library.link/vocab/creatorName
Butler, Ricky W
Funding information
Sponsored by the National Aeronautics and Space Administration
Government publication
federal national government publication
Illustrations
illustrations
Index
no index present
Literary form
non fiction
Nature of contents
  • dictionaries
  • bibliography
  • technical reports
http://library.link/vocab/relatedWorkOrContributorName
Langley Research Center
Series statement
NASA technical memorandum
Series volume
110274
http://library.link/vocab/subjectName
  • Hardware
  • Proving
  • Bit synchronization
  • Integers
  • Libraries
Type of report
Technical memorandum.
Label
A bitvectors library for PVS, Ricky W. Butler [and four others]
Link
http://purl.fdlp.gov/GPO/gpo75879
Instantiates
Publication
Distribution
Note
  • "August 1996."
  • "Performing organization: National Aeronautics and Space Administration Langley Research Center"--Report documentation page
  • Available online
Antecedent source
file reproduced from original
Bibliography note
Includes bibliographical references (pages 16-17)
Carrier category
online resource
Carrier category code
cr
Carrier MARC source
rdacarrier
Color
black and white
Content category
text
Content type code
txt
Content type MARC source
rdacontent
Control code
ocn844605585
Dimensions
unknown
Extent
1 online resource (17 pages)
File format
one file format
Form of item
online
Media category
computer
Media MARC source
rdamedia
Media type code
c
Other physical details
illustrations.
Specific material designation
remote
Label
A bitvectors library for PVS, Ricky W. Butler [and four others]
Link
http://purl.fdlp.gov/GPO/gpo75879
Publication
Distribution
Note
  • "August 1996."
  • "Performing organization: National Aeronautics and Space Administration Langley Research Center"--Report documentation page
  • Available online
Antecedent source
file reproduced from original
Bibliography note
Includes bibliographical references (pages 16-17)
Carrier category
online resource
Carrier category code
cr
Carrier MARC source
rdacarrier
Color
black and white
Content category
text
Content type code
txt
Content type MARC source
rdacontent
Control code
ocn844605585
Dimensions
unknown
Extent
1 online resource (17 pages)
File format
one file format
Form of item
online
Media category
computer
Media MARC source
rdamedia
Media type code
c
Other physical details
illustrations.
Specific material designation
remote

Library Locations

Library Links

Processing Feedback ...