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

指针是用于定义动态增长和递归数据结构的编程语言的一个重要特性。许多语言不仅提供指向数据的指针，还提供指向函数或过程的指针，即指向可执行代码的指针。在高级语言中，代码指针可能以函数指针的形式显式地表现出来，或者以伪装的形式出现，例如，作为携带自己方法集的对象的方法。因此，函数指针在运行时为代码组织提供了高度的灵活性，但由于其复杂性，它们在规范和验证中的意义很差。为了为现代和未来的语言构建正确的软件，具有允许对包括函数指针在内的程序进行推理的逻辑是至关重要的。重要的是，推理是局部的和模块化的，这意味着验证可以简单地在受一段代码影响的堆部分完成，并且独立于稍后阶段将分别链接的其他代码。为代码指针开发这样的推理原则，并将它们伪装成元编程特性（如运行时生成和加载代码），这是本项目的目标。在软件生产中，大量的时间用于测试程序没有错误，因此不会显示出不希望的甚至有害的行为。虽然测试只与测试数据一样好，但更严格的方法是验证程序是否符合特定的规范，例如，它不会导致内存错误。然而，包含指针的程序是出了名的难以指定，更不用说验证了。正如Tony Hoare爵士在1973年所说的那样：在高级语言中引入指针是一种倒退，我们可能永远无法恢复。30年后，指针和引用仍然是重要的语言特性，程序验证仍然是代价高昂的例外。但是最近的分离逻辑（由Reynolds， O'Hearn和其他人）的发展终于为我们提供了一个处理指针复杂性的方法。它允许在堆上进行局部推理，从而使验证者不必在执行过程或命令时指定和证明堆的大部分不会改变。唉，到目前为止，只有一阶数据（如数字或字符串）上的指针受益于最近的增强。函数指针同样有用。它们通常用于实现事件处理或自动软件配置。使用哪个处理程序（作为回调）取决于注册的函数指针的内容，即在运行时分配。代码的动态调用，类似于面向对象语言中的动态调度，也可以通过这样的指针来实现。因此，函数指针不仅仅是一种稀有的东西。事实上，它们很常见，出现在ML或C语言中。c#语言甚至为它们提供了一个特殊的类型结构：委托。在Java中，这些可以通过单方法接口来模拟。然而，接口并不仅仅通过类型签名来标识方法，这使得跨库共享它们变得困难。Java开发人员通过创建动态包装器对象（代理）来解决这个问题。这是Reflection原则的典型实例，它表示在编程语言中进行内省、调解和生成代码的能力，从而构成元编程方法。另一个重要的反射原理是动态加载，它允许在运行时加载代码模块（例如用于扩展功能的软件插件）。对于这些高级特性（其中一些在标准的面向对象语言中还没有），没有足够的程序逻辑。因此，这个项目的中心目标是为具有显式和隐式代码指针的语言建立程序（Hoare-）逻辑，使分离逻辑的好处适用于它们。

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.