This book starts by introducing the different definitions/theorems for semantic equivalence and analysis them proving problems in them all. Then, it develops a sound definition and theory for semantic equivalence that is congrunt and develops a formal method to prove the equivalence. It then develops formal methods for automated derivation of testing sequences. These cover both control flow and data flow. These methods are proven to have the widest applicability and coverage in terms of discovering errors if there are. Then, we develop formal methods to transform formal specifications...