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.

  • 1
    $\begingroup$ 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? $\endgroup$ – Andrej Bauer Aug 3 '11 at 10:01
  • 5
    $\begingroup$ 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). $\endgroup$ – Andrej Bauer Aug 3 '11 at 10:02
  • $\begingroup$ @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. $\endgroup$ – Yuning Aug 3 '11 at 10:13
  • 4
    $\begingroup$ This resembles the control flow graph one finds in (imperative language) compiler internals. $\endgroup$ – Dave Clarke Aug 3 '11 at 10:56
  • $\begingroup$ This sounds slightly similar to what I am trying to do saltyschemer.posterous.com/… $\endgroup$ – Joshua Herman Aug 3 '11 at 12:05

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.

  • $\begingroup$ To my understanding, lattices in Cousot^2 paper has little to do with the language definition. Lattices are used in the abstract interpretation essentially to handle the (computation of approximation of) semantics at the points where multiple execution paths join together (aka meet). But indeed Section 4 of Cousot^2 paper, and Section 2.1 in Gulwani & Tiwari's paper provide the definitions a la OP question. $\endgroup$ – user17 Aug 4 '11 at 4:08
  • $\begingroup$ 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. $\endgroup$ – Vijay D Aug 4 '11 at 13:26
  • $\begingroup$ Oh, I didn't know the context of OP's other question! $\endgroup$ – user17 Aug 4 '11 at 13:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.