Weakest pre-condition reasoning for Java programs with JML annotations

Bart Jacobs. Weakest pre-condition reasoning for Java programs with JML annotations. Journal of Logic and Algebraic Programming, 58(1-2):61-88, 2004. [doi]

Abstract

Abstract is missing.