LEADER 02214oam  2200517   450 
001 9910707834703321
005 20161223141253.0
035   $a(CKB)5470000002468213
035   $a(OCoLC)844605585
035   $a(EXLCZ)995470000002468213
100   $a20130526j199608    ua             0
101 0 $aeng
135   $aurbn||||a|a||
181   $ctxt$2rdacontent
182   $cc$2rdamedia
183   $acr$2rdacarrier
200 12$aA bitvectors library for PVS /$fRicky W. Butler [and four others]
210   $aWashington, D.C. $cNational Aeronautics and Space Administration$d1996
210  1$aHampton, Virginia :$cNational Aeronautics and Space Administration, Langley Research Center,$dAugust 1996.
215   $a1 online resource (17 pages) $cillustrations
225 1 $aNASA technical memorandum ;$v110274
300   $a"August 1996."
300   $a"Performing organization: National Aeronautics and Space Administration Langley Research Center" Report documentation page.
320   $aIncludes bibliographical references (pages 16-17).
330   $aThis 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.
606   $aHardware$2nasat
606   $aProving$2nasat
606   $aBit synchronization$2nasat
606   $aIntegers$2nasat
606   $aLibraries$2nasat
615  7$aHardware.
615  7$aProving.
615  7$aBit synchronization.
615  7$aIntegers.
615  7$aLibraries.
700   $aButler$b Ricky W.$01398460
712 02$aLangley Research Center,
801  0$bOCLCE
801  1$bOCLCE
801  2$bOCLCO
801  2$bOCLCQ
801  2$bGPO
906   $aBOOK
912   $a9910707834703321
996   $aA bitvectors library for PVS$93549741
997   $aUNINA