Working the Coq Theorem Prover, we defined and proved properties for the programming language IMP, a simple imperative language. We implemented a graph model denotational semantics and found that our definition resulted in full abstraction and semantic coincidence with IMP's generally accepted operational semantics. By constructing this graph model, IMP programs can now be mapped to partial functions that, using a fixed point operator, enable us to reason about potentially non-terminating algorithms.