A Bitvectors Library for PVS
W Butler Ricky, S Miner Paul, K Srivas Mandayam, A Greve Dave, P Miller Steven · NASA Technical Reports Server (NASA) · 1996
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.