Abstract: The corresponding relation between predicate transformers and state transformers has been studied. We treat the imperative denotations as predicate transformers to specify the denotational semantics of programming language IMP, and predicate transformers

Key words: Predicate transformers, State transformers, Denotational semantics