is there a formal algebra method to analyze programs?

Is there a formal/academic connection between an imperative program and algebra, and if so where would I learn about it?

The example I'm thinking of is:

``````if(C1) { A1(); A2(); }
if(C2) { A1(); A2(); }
``````

Represented as a sum of terms:

``````(C1)(A1) + (C1)(A2) + (C2)(A1) + (C2)(A2) = (C1+C2)(A1+A2)
``````

The idea being that manipulation could lead to programatic refactoring - "factoring" being the common concept in this example.

-
Formal Methods are a whole area of research in the Computer Science field. I know I did a course on them when I got my MS. Are you looking for specific references? – Matthew Flynn Mar 20 '12 at 21:36
i'm looking for some way to view the logic of a program independent from it's implementing programming language... higher level than a theoretical tape or stack based VM... it's probably a pipe dream but just the same I appreciate the link so I have a connection to something real – Aaron Anodide Mar 20 '12 at 21:39
@Gabriel There are many such higher level languages. Process algebra, Z, even Alloy are languages for modeling computer programs. However, you also need something that can extract the model from code so that it can be analyzed. But search for Symbolic Execution of Java Bytecode for an example paper doing roughly what you want. Due to the complexity, most analyzers are sort of dumb. But beyond symbolic execution, you have concolic (symbolic+concrete) execution. Anyway, researching formal methods is a reasonable starting point. – ccoakley Mar 21 '12 at 0:47
@Gabriel: Also, you should probably look at ML. The language was developed almost for the explicit purpose of being easy to analyze. Robin Milner provided a very rigorous mathematical definition of all of the semantics of the language. As far as "logic of a program independent from it's implementing programming language," I'm not sure what you mean. Even a simple if construct cannot easily be analyzed independent of implementation language. Do "and" and "or" short circuit? What values can be coerced to True and False (and null)? Is if a statement or an expression? – ccoakley Mar 21 '12 at 0:56
Ok .. so are these answers or are you just writing comments? this is why we have an answer section peeps. – Ross Mar 21 '12 at 11:44

As others have pointed out there is a lot of existing research into formal methods for program analysis. A former colleague of mine is an active researcher in this area and his page gives several pointers on where to start.

There are several keywords in that area, each of which basically spawns a whole research area itself. Hence, your question cannot be fully answered here, but we can at least provide some direction. For the most part, these approaches are separated into three branches:

• Algebraic semantics are one way of giving semantics to programming languages via different algebras. See the wikipedia article for an overview. Things like Kleene algebras or Omega algebras fit in there.
• Operational semantics are quite popular calculi to model behaviors (for example, the lambda calculus, or LISP)
• Denotational semantics rely on a fitting domain. They include, for example, approaches rooted in predicate or linear logic (think Prolog or more advanced languages like CHR).

And just like in physics we are also interested in unifying these branches, at which point you enter the realms of the unified theories of programming.

Sorry for not giving a specific answer to the question, but there's enough material available for all of this to keep you busy for a few decades, and unless a desired application is in mind it's not really possible to make a choice from these.

-
very helpful answer, thanks for all the references! – Aaron Anodide Apr 11 '12 at 21:07