Checking Whether Programs Are Correct or Incorrect.

摘要

A program is considered as consisting of two parts, an algorithm part and a specification part, where the latter records the programmer's intentions as to how the algorithm should work. The question of what is a proper notion of semantic correctness for such programs is discussed, the emphasis being on finding a criterion which supports the construction and maintenance of correct programs. For a suitable notion of semantic correctness, a system to check it for programs is described. This system will either declare a program to be semantically correct, or it will show it to be incorrect by exhibiting a semantic error. (ERA citation 07:045442)