权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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

从函数指针的推理原理到自配置程序的逻辑

基本信息

批准号：
EP/G003173/1
负责人：
Bernhard Reus
金额：
$ 49.8万
依托单位：
University of Sussex
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2008
资助国家：
英国
起止时间：
2008 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FG003173%2F1
关键词：
Reasoning Principles Function Pointers Logics

项目摘要

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.

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