Academic Press
Information and Computation

America, P., & de Boer, F. (1990). Proving total correctness of recursive procedures. Information and Computation, 84(2), 129–162.