Semantic subtyping for imperative object-oriented languages