JUCS - Journal of Universal Computer Science 3(10): 1121-1125, doi: 10.3217/jucs-003-10-1121

A Note on Correctness Proofs for Overflow Detection Logic in Adders for d-th Complement Numbers

‡ Telekom Entwicklungszentrum Südwest, Saarbruecken, Germany§ FernUniversität in Hagen, Hagen, Germany

Corresponding author: Bernd Rederlechner ( bernd.rederlechner@ezsw.telekom.de ) © Bernd Rederlechner, Jörg Keller. This article is freely available under the J.UCS Open Content License. Citation:
Rederlechner B, Keller J (1997) A Note on Correctness Proofs for Overflow Detection Logic in Adders for d-th Complement Numbers. JUCS - Journal of Universal Computer Science 3(10): 1121-1125. https://doi.org/10.3217/jucs-003-10-1121 |

Abstract

When adding n-bit 2-th complement numbers, the result can be outside the range representable with n bits. A well-known theorem justifies the common overflow logic: Let a,b {0,1}n be the 2-th complement representations of signed integers [a] and [b], respectively, and let c0 {0, 1} be the carry-in bit. Then, [a] + [b] + c0 {-2n-1,...,2n-1-1} if and only if cn = cn-1 , where ci denotes the carry-bit 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 d-th 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 re-invention.

Keywords

d-ary arithmetic, correctness proof, computer science education, overflow testing