Refinement calculi for imperative programs provide an integrated framework for programs and specifications and allow one develop programs from specifications in a systematic fashion. The semantics of these calculi has traditionally been defined in terms of predicate transfoermers and poses several challenges in defining a state transformer semantics in the denotational style. We define a novel semantics in terms of sets of state transformers and prove it to be isomorphic to positively multiplicative predicate transformers. The semantics disagrees with the traditional semantics in some places and the consequences of the disagreement are analyzed.