
A Note on Correctness Proofs for Overflow Detection Logic in Adders for dth Complement Numbers
Bernd Rederlechner (Telekom Entwicklungszentrum Südwest, Germany)
Jörg Keller
Abstract: When adding nbit 2th complement numbers, the result can be outside the range representable with n bits. A wellknown theorem justifies the common overflow logic: Let a,b {0,1}n be the 2th complement representations of signed integers [a] and [b], respectively, and let c0 {0, 1} be the carryin bit. Then, [a] + [b] + c0 {2n1,...,2n11} if and only if cn = cn1 , where ci denotes the carrybit from position i  1 to position i when adding the binary numbers a and b. We present a proof of this theorem which is much shorter than previous proofs. This simplification can save valuable time in computer science classes. With a small extension the proof even holds for dth complement numbers. Although the proof technique is known by some specialists, nobody seems to have written it up. With this note, it is once documented in a precise form, thus avoiding reinvention.
Keywords: computer science education, correctness proof, dary arithmetic, overflow testing
Categories: B.2, K.3.2
