|
|
|---|
|
|
|
|---|
Definitions and lemmas about logical operations on integers.
The books logops-definitions and logops-lemmas contain a theory of the logical operations on numbers defined by CLTL (Section 12.7), and a portable implementation of the CLTL byte manipulation functions (Section 12.8). These books also extend the CLTL logical operations and byte manipulation theory with a few new definitions, lemmas supporting those definitions, and useful macros.
These books were developed as a basis for the formal specification and verification of hardware, where integers are used to represent binary signals and busses. These books should be general enough, however, to be used as a basis for reasoning about packed data structures, bit-encoded sets, and other applications of logical operations on integers.