Correctness of Programs

The semantics of programs was a prelude necessary to make explicit exactly what programs do. The direction of this book now turns to the central issue: how to establish that a program does the right things. It is assumed to begin with that programs are syntactically correct. The detection of syntax errors—missing parentheses and the like—belongs to the study of formal languages. Here the issue is detecting semantic errors incorrect loop initialization and the like.