Have imperative programs been defined like this?
Short answer: yes.

Longer answer -- there probably isn't a unique reference but control flow graphs (essentially what you describe) and their precursors, flowcharts are Old. Here are three random references from antiquity to something very recent that use minor modifications of the model. The latter two define the model fairly precisely. You'll find a lot of lattices in the second paper.


Assigning Meaning to Programs, Robert Floyd, 1967.
Systematic Design of Program Transformation Frameworks by Abstract Interpretation, Patrick Cousot and Radhia Cousot, POPL 2002.
Assertion Checking Unified, Sumit Gulwani and Ashish Tiwari, VMCAI 2007.