References

The JML web site contains a long list of papers relevant to JML and to program specification and verification. I won't duplicate that here. Instead the papers listed here are those particularly relevant to how a tool like OpenJML is built and to the specific features in JML

THIS LIST IS VERY MUCH A WORK IN PROGRESS

Arithmetic

P. Chalin,
JML Support for Primitive Arbitrary Precision Numeric Types: Definition and Semantics, JOT, 3(6):57-79, 2004.