Peter Bancroft: Module refinement refined (for the calculation of Oberon programs). University of Queensland, Australia 1997