The semantic formalisms presented in Chapter 7 define the meaning of programming languages and thus implicitly also of computer programs written in these languages. However, they are too low-level to be of practical use when our actual goal is to verify the correctness of a program with respect to its specification. In this chapter, we are going to discuss various (closely related) calculi that allow us to reason about programs on this high level.