Program correctness on finite fields

Abstract 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.; Accession Number: 15036701; Authors: Csirmaz, László 1; Author Affiliations: 1: Mathematical Institute of the Hungarian Academy of Sciences H-1364 P.O. Box 127 Budapest Hungary H-1364 P.O. Box 127 Budapest Hungary