Idealized coinductive type systems for imperative object-oriented programs