Have imperative programs been defined like this?

Possibly improper definition $\;$ An imperative program is a labeled directed graph, with every vertices labeled by a command and every edge labeled by a predicate.

Denote an edge labeled by predicate $p$ from $x$ to $y$ by $(x, p, y)$,

• Two consecutive steps are expressed as $(x, \top, y)$. "Goto" is also expressed in this way.
• A binary branch is expressed as $\{(x, p, y), (x, \neg p, z)\}$.

As can be easily noticed, "command" is not defined. I do not know what that should be, but it should be as weak as possible.

Have imperative programs been defined like that?

I also think a mathematical definition could help me go further understanding the space of imperative programs.

• This is at best an incomplete description of something. Is there supposed to be state (variables)? Is there a starting node? What happens if the next transition is not determined uniquely? – Andrej Bauer Aug 3 '11 at 10:01
• Oh, and by the way, it looks like flow-chart diagrams, except you draw them a bit differently (by putting conditional statements onto the edges). – Andrej Bauer Aug 3 '11 at 10:02
• @AndrejBauer, there could(should?) be states, but it seems there can be different ways to do that while keeping the defined part valid. I am aware of the uniqueness issue, but I wonder leaving it as is might be acceptable. – Yuning Aug 3 '11 at 10:13
• This resembles the control flow graph one finds in (imperative language) compiler internals. – Dave Clarke Aug 3 '11 at 10:56
• This sounds slightly similar to what I am trying to do saltyschemer.posterous.com/… – Joshua Herman Aug 3 '11 at 12:05