Program correctness on finite fields
Program correctness on finite fields
L. 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.