Modularity and Resource Separation

模块化和资源分离

基本信息

批准号：
EP/D053625/1
负责人：
Peter O'Hearn
金额：
$ 35.37万
依托单位：
Queen Mary University of London
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2006
资助国家：
英国
起止时间：
2006 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FD053625%2F1
关键词：
Modularity Resource Separation

项目摘要

Modularity is a key concept which programmers wield in their struggle againstthe complexity of software systems. When a program is divided into conceptually distinct modules or components, each of which uses separate internal resources (such as storage),the effort required for understanding the program is decomposed into circumscribed, hopefully manageable, parts. The purpose of this project is to bring separation logic to bear on modularity.The separating conjunction connective will be used to give a precise, theoretical expression that correspondsto the existing pre-formal, intuitive link between resource separation and modularity.We will develop semantic models that describe when a piece of state used by a module is held separate from the clients that use it. Theories of refinement and parametricity will be studied. The former will begin to address one of the common criticisms of separation logic,that verifications take place on a fixed (low) level of abstraction. The latter will give us methods for showing equivalence of imperative modules and for understanding information hiding for imperative resources. We will also investigate methods for proof and static checking and analysis for imperative modules. This project contribute considerably to the problems of scalable reasoning about programs and protection of resources from outside tampering, in the presence of practical programming features such as pointers thathave previously been seen as barriers to technically precise accounts of modularity.

模块化是一个关键概念，程序员在与软件系统的复杂性的斗争中发挥作用。当一个程序在概念上不同的模块或组件分为不同的模块或组件时，每个模块或组件都使用独立的内部资源（例如存储）时，理解该程序所需的精力被分解为限制，希望可管理的部分。该项目的目的是将分离逻辑带到模块化上。分离连接连接将用于提供精确的，理论上的表达，以对应现有的正式前，资源分离和模块化之间的直觉，直观的联系。我们将开发语义模型它描述了何时将模块使用的状态与使用它的客户分开。将研究改进和参数的理论。前者将开始解决对分离逻辑的普遍批评之一，即验证是在固定（低）抽象水平上进行的。后者将为我们提供显示命令模块等效性以及理解隐藏命令资源的信息的方法。我们还将研究用于证明和静态检查和分析命令模块的方法。在存在实用的编程功能（例如以前被视为技术上精确说明模块化的障碍）的情况下，该项目有助于有关计划和保护资源免受外部篡改的可扩展推理的问题。