From Reasoning Principles for Function Pointers To Logics for Self-Configuring Programs

Pointers are an important feature of programming languages used to define dynamically growing and recursive data structures. Many languages provide pointers not just to data but also functions or procedures, i.e. to executable code. In high-level languages code pointers may manifest themselves explicitly in the form of function pointers or appear in disguises, e.g. as methods of objects carrying their own method suites. Thus, function pointers offer high flexibility of code organisation at runtime but their meaning in specification and verification has been poor due to their complexity. In order to build correct software for modern and future languages it is paramount to have logics that permit reasoning about programs including function pointers. It is important that reasoning is local and modular which means that verification can be done simply w.r.t. the part of the heap affected by a piece of code, and independently of other code that is going to be linked at a later stage, respectively.To develop such reasoning principles for code pointers and their disguised appearance as meta-programming features like run-time generation and loading of code is the objective of this project.In software production a huge amount of time goes into testing that programs are free from errors and thus do not show undesired or even harmful behaviour. While testing is only as good as the test data is, a much more rigorous approach is to verify that a program meets a certain specification, for example that it does not lead to memory faults. Programs containing pointers, however, are notoriously difficult to specify, let alone verify. As Sir Tony Hoare said back in 1973: The introduction of pointers into high-level languages has been a step backwards from which we may never recover.'' 30 years later pointers and references are still important language features and program verification is still the costly exception. But the recent development of Separation Logic (by Reynolds, O'Hearn and others) has finally presented us with a handle to tackle the complexity of pointers. It permits local reasoning on the heap, liberating the verifier from specifying and proving that most of the heap does not change when a procedure or command is executed. Alas, so far only pointers on first-order data like numbers or strings profit from this recent enhancement.Function pointers are equally useful however. They are often employed to implement event handling or automatic software configuration. Which handler is used (as callback'') depends on the content of the function pointer registered, i.e. assigned at runtime. Dynamic invocation of code, reminiscent of dynamic dispatch in object-oriented languages, can also be achieved via such pointers. Function pointers are therefore not simply a rare curiosity. In fact, they are commonplace and appear in languages like ML or C. The language C# even has a special type construct for them: delegates. In Java these can be simulated via single method interfaces. Interfaces, however, do not identify methods by type signatures alone which makes it hard to share them across libraries. Java developers address this by creating on-the-fly wrapper objects (proxies).This is a typical instance of a principle called Reflection that denotes the ability to introspect, intercede, and generate code in a programming language and thus constitutes a method of meta-programming. Another important reflection principle is dynamic loading which allows code modules (for instance software plugins for extended functionality) to be loaded at runtime. For such advanced features, some of which are not available in standard object-oriented languages yet, there are no adequate program logics. Therefore, the central objective of this project is to establish program (Hoare-) logics for languages with explicit and implicit code pointers making the benefits of Separation Logic amenable to them.