<p>Short answer: yes.</p>

<p>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.</p>

<ul>
<li><a href="http://www.eecs.berkeley.edu/~necula/Papers/FloydMeaning.pdf" rel="nofollow">Assigning Meaning to Programs</a>, Robert Floyd, 1967.</li>
<li><a href="http://www.di.ens.fr/~cousot/COUSOTpapers/POPL02.shtml" rel="nofollow">Systematic Design of Program Transformation Frameworks by Abstract Interpretation</a>, Patrick Cousot and Radhia Cousot, POPL 2002.</li>
<li><a href="http://research.microsoft.com/en-us/um/people/sumitg/pubs/ac_unified.pdf" rel="nofollow">Assertion Checking Unified</a>, Sumit Gulwani and Ashish Tiwari, VMCAI 2007.</li>
</ul>

CC BY-SA 3.0
2011-08-04T13:26:51.030Z
Hello M. S. The lattice comment was in reference to the link the OP gave to another question about lattices of programs. The lattice does depend on the datatypes of the language. Statements define transformers. I agree that the lattice is semantic. Finding a lattice structure is difficult if you have arbitrary control flow graphs.
Vijay D
CC BY-SA 3.0
2011-08-04T02:06:36.657Z
2011-08-04T02:06:36.657Z
Vijay D
<p><strong>Possibly improper definition</strong> $\;$ An imperative program is a labeled directed graph, with every vertices labeled by a command and every edge labeled by a predicate.</p>

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

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

<p>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.</p>

<p><strong>Have imperative programs been defined like that?</strong></p>

<p>I also think a mathematical definition could help me go further understanding <a href="https://cstheory.stackexchange.com/questions/7505/space-of-imperative-programs">the space of imperative programs</a>.</p>

CC BY-SA 3.0
2011-08-03T10:01:43.907Z
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
CC BY-SA 3.0
2011-08-03T10:02:58.943Z
Oh, and by the way, it looks like [flow-chart diagrams](http://en.wikipedia.org/wiki/Flowchart), except you draw them a bit differently (by putting conditional statements onto the edges).
Andrej Bauer
CC BY-SA 3.0
2011-08-03T10:13:16.533Z
@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
CC BY-SA 3.0
2011-08-03T10:56:42.970Z
This resembles the [control flow graph](http://en.wikipedia.org/wiki/Control_flow_graph) one finds in (imperative language) compiler internals.
Dave Clarke
CC BY-SA 3.0
2011-08-03T12:05:44.143Z
This sounds slightly similar to what I am trying to do http://saltyschemer.posterous.com/rethinking-geometric-complexity-theory
Joshua Herman
<reference-request><imperative-programming>
Have imperative programs been defined like this?
Yuning
# Have imperative programs been defined like this?

(Asked by: username_0 on 2011-08-03)

**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](https://cstheory.stackexchange.com/questions/7505/space-of-imperative-programs).

**Tags:** reference-request, imperative-programming
> **Comments:**
> **username_1**: 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?  
> **username_1**: Oh, and by the way, it looks like [flow-chart diagrams](http://en.wikipedia.org/wiki/Flowchart), except you draw them a bit differently (by putting conditional statements onto the edges).  
> **username_0**: @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.  
> **username_2**: This resembles the [control flow graph](http://en.wikipedia.org/wiki/Control_flow_graph) one finds in (imperative language) compiler internals.  
> **username_3**: This sounds slightly similar to what I am trying to do http://saltyschemer.posterous.com/rethinking-geometric-complexity-theory  

---

## 1 answers

### Answer by username_4 on 2011-08-04. Score: 3 | Accepted answer

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](http://www.eecs.berkeley.edu/~necula/Papers/FloydMeaning.pdf), Robert Floyd, 1967.
* [Systematic Design of Program Transformation Frameworks by Abstract Interpretation](http://www.di.ens.fr/~cousot/COUSOTpapers/POPL02.shtml), Patrick Cousot and Radhia Cousot, POPL 2002.
* [Assertion Checking Unified](http://research.microsoft.com/en-us/um/people/sumitg/pubs/ac_unified.pdf), Sumit Gulwani and Ashish Tiwari, VMCAI 2007.

> **Comments:**
> **username_4**: Hello M. S. The lattice comment was in reference to the link the OP gave to another question about lattices of programs. The lattice does depend on the datatypes of the language. Statements define transformers. I agree that the lattice is semantic. Finding a lattice structure is difficult if you have arbitrary control flow graphs.  

---

