Specifying and Checking Refinement Relationships in VDM++. - Yojiro Kawamata; Christian Sommer 001; Fuyuki Ishikawa; Shinichi Honiden (SEFM, 2009)