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

• Autore: Butler Ricky W.
• Pubblicazione: Washington, D.C., : National Aeronautics and Space Administration, 1996; Hampton, Virginia : , : National Aeronautics and Space Administration, Langley Research Center, , August 1996
• Descrizione fisica: 1 online resource (17 pages) : illustrations
• Soggetto topico: Hardware; Proving; Bit synchronization; Integers; Libraries
• Note generali: "August 1996."; "Performing organization: National Aeronautics and Space Administration Langley Research Center" Report documentation page.
• Nota di bibliografia: Includes bibliographical references (pages 16-17).
• Sommario/riassunto: 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.
• Titolo autorizzato: A bitvectors library for PVS
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Lingua di pubblicazione: Inglese
• Record Nr.: 9910707834703321
• Lo trovi qui: Univ. Federico II