Tweeted twitter.com/StackCompSci/status/977554685015023617
2 edited tags
| link
1
source | link

Formal basis for "peephole reasoning" about code

The approaches I've seen to abstractly talking about the semantics of a programming language like Turing machines, various lambda calculi, and Hoare logic seem to be talking about the behavior of entire programs / entire expressions. Lambda calculus does regularly involve free variables, perhaps it isn't the best example.

As a programmer though, you spend a lot of time looking at fragments of code and trying to understand what they do. In those situations though, you usually have some knowledge about the project / collection of code as a whole (e.g. it builds without errors).

In particular, in many languages it makes sense to think about "where control currently is right now" and "where control will be transferred to given what I know".

if (x) {
    foo(x);
} else {
    bar(x);
}

If this is part of a C file, we have some very strong guarantees about where control is transferred to if x is some non-zero-y value in whatever type it has*. It either go to the function named foo (either a static one in our same translation unit) or else the non-static function named foo in our project. Since the project builds we know there can only be one.

In C++, for example, we can dispatch on the type that x statically has in this context here. Because foo is a free function, we know that it can't be virtual, so we still don't need to know very much about the value that x has at runtime, just whether operator bool produces true or false.

That example has way too much detail imported from the real world. (It's also probably not totally accurate). We've talked a little bit about separate compilation and constructed some kind of informal mapping between the dynamic behavior of the program and its static representation in order to talk about the flow of control through a program.

The point of this was to make a comparison between C and C++ ... namely that C does not require you to know as much in order to determine where control is transferred to.**

Being able to make a few assumptions and then start proving things about regions of code, regardless of what the rest of the code is, seems like a powerful technique.

I'm wondering what approaches people have taken to formalizing it and what they've called it so I can read more about what they've done.

*For the moment, I am ruling out the possibility that foo, bar, or x are macros.

**I'm implicitly treating C as a subset of C++, which isn't strictly accurate.