Correctness Theories and Program Equivalence

摘要

The mathematical concept that a programming language semantics can be sensibly determined by proof rules for the before-after assertions required true of programs in the language was investigated. It is shown that the theory of program correctness based on first order logic can in a natural way specify the basic semantical concept of program equivalence in the case of programs terminating throughout any given class of data structures, but that diverging programs require rather delicate investigations into the associated classes.