Abstract

The aim of this note is to present some recent results concerning the nonstandard approach to program correctness. The reader is supposed to be familiar with the basic notation of program and program verication as well as the model theory. The concepts used here are basically from [2] and [4]. The denitions of program, program run, etc. given here are rather sketchy and expected to give only a general idea of these notions; the results, however, remain true under a wide range of other denitions, cf. [1], [3], [5]