Program interpretation for static analysis

Question

Are there any implementations, or even academic work, regarding an application capable of looking at code and inferring what the code actually intends to do? For example, we give it a program that calculates the SQRT(x); it should go and annotate that particular piece of code with SQRT(X), regardless of implementation technique. Say you use recursion instead of a for loop; it should still be able to infer what the code intends to do. Pattern matching is not really an option here.

Another example: Say you have a program that computes the sum of inverse squares, starting at 0. It should print out the mathematical equivalent of that expression as result. Something like SIGMA 1/x^i

Answer 1

It's been hinted at in the comments, but in general, the task of giving non trivial explanations of an arbitrary piece of code by some automated analysis is impossible.

The first issue is giving a well-defined meaning to the term "program intent". The field of operational semantics can give us a precise definition of what a piece of code actually does when run on a concrete computer, under the hypothesis that the compiler or interpreter is free of programing errors, but the intent of the person who wrote the code can obviously not be divined from the code itself, e.g. a piece of code may be intended to say, crash if given a negative number as input, or that outcome may be the result of programmer oversight.

However it might be desirable to, say, infer various mathematical properties of an arbitrary piece of code, in your example you might want to infer

forall x, if x > 0 then SQRT(x)*SQRT(x) == x

This also is impossible to do in general. This somewhat surprising fact can be demonstrated using Rice's theorem, which essentially says that any property like the above statement can not be proven or refuted automatically for arbitrary programs.

That being said, there has been a substantial body of work which aims at identifying and proving properties such as the above for concrete program implementations. Because of Rice's theorem, such attempts must be incomplete, but in practice much can be done for "real world" programs. This field is usually designated under the term formal methods, and even a short summary would be significantly more effort than I'm ready to put forward right now. A good overview can be found here.

Answer 2

This is essentially impossible. Not only for programming languages, but for natural languages like English, even. For example, Google Translate can't actually determine the essence of what you are trying to say. All Google Translate does in reality is match a pattern (syntax recognition) with a few bells a whistles in the form of allowing for synonymous terms and phrases etc, to allow for more flexibility.

The extent to which semantic analysis is effective is actually very limited. Your question implied compiler implementation as the means to achieve some sort of semantic (meaning) derivation from any given program. The compiler can analyze tokens (words, symbols), then match a specific pattern of those tokens and label it as 'Expression' or 'Class' or 'VarDecl' or whatever, then it will analyze whether those recognized patterns are in the correct order, make sense in consideration of the particular context, whether it could be substituted for an equivalent expression of that same structure.

But as you can imagine, there is only a finite amount of rules you can instruct the compiler to recognize. But to attempt to build a compiler that can extract the ultimate meaning of your program is expecting it to do something that sometimes even humans can't do perfectly.

Sometimes we really underestimate the power of the human mind to extract meaning. To try and implement that functionality in a program is much like trying to implement a program which can really understand abstract things like a movie's meaning. Or a song. We just aren't at that level yet.

Again, you can implement a small, finite set of rules which allow your program to express one thing in many forms, but this is pattern matching. And essentially all semantic analysis is still pattern matching.

There is currently no algorithm computers can understand which can work with real abstractions. All of them are pattern-matching type algorithms which, ultimately can't recognize anything they aren't written to. Real abstraction would be necessary for truly determining the meaning of a program. That said, there is a LOT a compiler does to recognize structures and replace them, optimize them, completely remove them etc. - to the point where there isn't much need for them to understand what is being done as a whole. In fact, I don't think there are many programmers good enough to know how to replace a program as a whole and write it better, most of the time. So, it follows that the programmer responsible for writing a program capable of such would have to be good enough to do that himself, and even then, this would be hard to write down.