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

Specifications that are used in detailed design and in the documentation of existing code are primarily written and read by programmers. However, most formal specification languages either make hea...