Axiomatic Semantics

Originally proposed by C. A. R. Hoare, axiomatic sematics define the meaning of a program by describing its effect on assertions about the program state. Axiomatic semantics is an approach based on mathematical logic to prove the correctness of computer programs.

For more information:

"An Axiomatic Basis for Computer Programming" (PDF) by C. A. R. Hoare, Communications of the ACM, Vol. 12, No. 10, October 1969.
"Axiomatic Semantics" (PDF), chapter 11 of Formal Syntax and Sematics of Programming Languages: A Laboratory Based Approach by Kenneth Slonneger and Barry L. Kurtz, Addison-Wesley, 1995.
Axiomatic Semantics (PDF) - author unknown