Laszlo Csirmaz:

      Program correctness on finite fields

An asserted program is presented whose correctness is provable by the
Floyd-Hoare-Naur method in each finite field separately, which, however,
admits no universal derivation, i.e. one which would work on all but
finitely many finite fields of a given characteristic. Also, it is proved
in general that if ``executing a program twice with the same input, the
outputs agree'' is a provable property, then the output of the program is
first order definable from the input.

Key words: Finite fields, pseudofinite fields, program correctness,
Floyd-Hoare derivation.