November 14, 1976 ACM Comput. Surv. , 8(3), 331–353 An introduction to proving the correctness of programs S. Hantler, J. King