A Theory of programming is intended to help in the construction of
programs that provably meet their specifications.  It starts with a
complete lattice of specifications, used as a domain for the semantics
of the programming language. The operators of the language are defined
as monotonic functions over this domain.  This paper presents a method
which enables us to derive an enriched semantics for the imperative
language. We show that the new definition of the primitive commands
can be recast as the weakest solution of the embedding equation, and
demonstrate how the operators of the programminbg language are
redefined from the homomorphic property of the embedding and the
healthiness conditions imposed on "real" programs.