The field of algebraic numbers fails to possess even a nice sound, if relatively incomplete, hoare-like logic for its while-programs : (preprint)
Jan Aldert Bergstra, John Vivian Tucker · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1980
Under a weak definition of a Hoare logic for while-programs, interpreted in a structure A, we show that many familiar structures fail to admit even a nice sound, if relatively incomplete, Hoare logic for the partial correctness of their while-program computations.Among our examples are Presburger Arithmetic, the field of real algebraic numbers, and the field of algebraic numbers.