General predicate transformer and the semantics of a programming language with go to statement

Dijkstra's predicate transformer for specifying the semantics of guarded commands set and proving the total correcness of a program is generalized to a programming language with the go to statement. The concept of general predicate transformer and its properties are introduced. We explore the approach of proving the correctness - preserving property of some common program transformations that are used in the compiling process.