JML Tutorial - Reasoning about program types TODO – examples of \type \typeof <: and difference from instanceof