A presentation of the research work accomplished at Oxford University on refinement calculus, which traces its rigorous development, from state-based assertional specifications, of executable imperative code. The attempts to bring together Z specifications and Dijkstra's language are discussed.