• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文学位 >Linear logic and imperative programming.
【24h】

Linear logic and imperative programming.

机译：线性逻辑和命令式编程。

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

One of the most important and enduring problems in programming languages research involves verification of programs that construct, manipulate and dispose of complex heap-allocated data structures. Over the last several years, great progress has been made on this problem by using substructural logics to specify the shape of heap-allocated data structures. These logics can capture aliasing properties in a concise notation.; In this dissertation, we present our work on using an extension of Girard's intuitionistic linear logic (a substructural logic) with classical constraints as the base logic to reason about the memory safety and shape invariants of programs that manipulate complex heap-allocated data structures. To be more precise, we have defined formal proof rules for an intuitionistic linear logic with constraints, ILC, which modularly combines substructural reasoning with general constraint-based reasoning. We have also defined a formal semantics for our logic -- program heaps -- with recursively defined predicates. Next, we developed verification systems using different fragments of ILC to verify pointer programs. In particular, we developed a set of sound verification generation rules that are used to statically verify pointer programs. We also demonstrated how to interpret the logical formulas as run-time assertions. In the end, we developed a new imperative language that allows programmers to define and manipulate heap-allocated data structures using ILC formulas.; The main contributions of this thesis are that (1) the development of a substructural logic that is capable of general constraint-based reasoning; and (2) the idea of incorporating high-level logical formulas into imperative languages; either as dynamic contract specifications, which allow clear, compact and semantically well-defined documentation of heap-shape properties; or as language constructs, which drive safe construction and manipulation of sophisticated heap-allocated data structures.
机译：编程语言研究中最重要，最持久的问题之一是验证构造，操纵和处置复杂的堆分配数据结构的程序。在过去的几年中，通过使用子结构逻辑来指定堆分配的数据结构的形状，在此问题上已取得了很大的进步。这些逻辑可以简明的方式捕获别名属性。在本文中，我们介绍了使用具有经典约束的吉拉德直觉线性逻辑（子结构逻辑）的扩展作为基础逻辑来推理操作复杂堆分配的数据结构的程序的内存安全性和形状不变性的工作。更准确地说，我们为带有约束的直觉线性逻辑（ILC）定义了形式化证明规则，该规则将子结构推理与基于常规约束的推理模块化地结合在一起。我们还为我们的逻辑（程序堆）定义了形式语义，并具有递归定义的谓词。接下来，我们开发了使用ILC的不同片段来验证指针程序的验证系统。特别是，我们开发了一组声音验证生成规则，用于静态验证指针程序。我们还演示了如何将逻辑公式解释为运行时断言。最后，我们开发了一种新的命令式语言，该语言使程序员可以使用ILC公式定义和操作堆分配的数据结构。本论文的主要贡献是：（1）能够基于一般约束推理的子结构逻辑的发展； （2）将高级逻辑公式合并到命令式语言中的想法；作为动态合同规范，它允许对堆状属性进行清晰，紧凑和语义明确的记录；或作为语言构造，可以安全地构造和操纵复杂的堆分配数据结构。

著录项

  • 作者

    Jia, Limin.;

  • 作者单位

    Princeton University.;

  • 授予单位 Princeton University.;
  • 学科 Computer Science.
  • 学位 Ph.D.
  • 年度 2008
  • 页码 254 p.
  • 总页数 254
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类 自动化技术、计算机技术;
  • 关键词

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号