A JML Tutorial: Modular Specification and Verification of Functional Behavior for Java