## Paper: Program Correctness on Finite Fields (at LICS 1986)

**László Csirmaz Bradd Hart**

### 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. on which would work on all but finitely many 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.

### BibTeX

@InProceedings{CsirmazHart-ProgramCorrectnesso, author = {László Csirmaz and Bradd Hart}, title = {Program Correctness on Finite Fields}, booktitle = {Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986)}, year = {1986}, month = {June}, pages = {4--10}, location = {Cambridge, MA, USA}, publisher = {IEEE Computer Society Press} }