How the design of JML accommodates both runtime assertion checking and formal verification

Gary T. Leavens, Yoonsik Cheon, Curtis Clifton, Clyde Ruby, David R. Cok. How the design of JML accommodates both runtime assertion checking and formal verification. Science of Computer Programming, 55(1-3):185-208, 2005. [doi]

Abstract

Abstract is missing.