Program State Transformer (II)
Jun He · Huadong Shifan Daxue xuebao. Ziran kexue ban · 1983
Dijkstra's predicate transformer for specifying the semantics of guarded commands set and proving the total correctness of a program is generalized to a programming language with a goto statement.The concept of program state transformer is used to derive some basic results for verification of programs_2 The approach of proving the correctness-preserving property of some common program transformations that are used in the compiling process is also explored.