Zhang, X., Munro, M., Harman, M., Hu, L., "Weakest precondition for general recursive programs formalized in coq", , 2002