Semantics and Data Refinement of Invariant Based Programs by Viorel Preoteasa and Ralph-Johan Back May 28