• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文学位 >Foundations for a tool for the automatic adaptation of software components based on semantic specifications.
【24h】

Foundations for a tool for the automatic adaptation of software components based on semantic specifications.

机译：基于语义规范自动适应软件组件的工具的基础。

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

摘要

We lay the foundations for a tool for the automatic adaptation of software components in call-by-value functional languages like Standard ML. Such a tool automatically generates simple adaptation functors that overcome minor incompatibilities between different but closely related signatures. The adaptation functors can be expressed in a typed λ-calculus with product types, ML-polymorphism and first-order type functions, but without recursion.; Component adaptation is based on semantic specification formulas. As it seems appropriate for functional programming languages, the semantic specifications are not pre-post-condition formulas. Instead, they are predicate logic formulas that treat functions in the same way as other values. For example, universal quantification over functions is allowed. Moreover, specification formulas pairs and projections. Specification formulas are similar, in style, to axioms in the wide spectrum language Extended ML (EML), but more restricted in order to facilitate automatic component adaptation. We study the semantics of specification formulas by interpreting them in a small call-by-value functional language. Predicates denote sets of closed expressions that are closed under observational equality.; A large part of the work consists of a high level description of methods for component adaptation. These methods come from the fields of automated theorem proving and typed λ-calculus, but substantial modifications are necessary for our purposes. Soundness proofs are provided for all of the methods and some completeness results are proved or conjectured. The investigation of the methods has three parts: Firstly, we study a classical logic sequent calculus whose term language is a recursion-free typed λ-calculus. Secondly, we study algorithms to decide subsets of observational equality for this term language. These include an algorithm that provides a better approximation of observational equality than βυπ υ-equality by allowing certain β-reductions that are not β υ-reductions, and an algorithm for deciding an extension of β υπυ-equality by value-restricted extensionality rules. Thirdly, we study βπ-unification for the term language. Extensions of known higher order unification procedures are necessary because our language has polymorphic existential variables and first order type functions. Moreover, unlike in most versions of higher order unification, we don't assume extensionality rules, because, unless value restrictions are imposed, they are unsound in a call-by-value language.
机译：我们为以值呼叫功能语言（例如ML）自动适应软件组件的工具奠定了基础。这种工具会自动生成简单的自适应函子，以克服不同但密切相关的签名之间的微小不兼容问题。自适应函子可以用具有产品类型，ML多态性和一阶类型函数的类型化λ微积分表示，但不递归。组件自适应基于语义规范公式。对于功能性编程语言而言，语义规范不是条件后的公式。相反，它们是谓词逻辑公式，它们以与其他值相同的方式对待函数。例如，允许对功能进行通用量化。此外，规格公式对和预测。规范公式在样式上与广谱语言扩展ML（EML）中的公理相似，但为了便于自动进行组件自适应而受到更多限制。我们通过用一种小型的按值调用功能语言来解释规范公式的语义来研究它们。谓词表示在观察相等性下闭合的闭合表达式集。大部分工作包括对组件适配方法的高级描述。这些方法来自自动定理证明和类型λ演算领域，但是对我们的目的而言，必须进行大量修改。提供了所有方法的健全性证明，并证明或推测了一些完整性结果。这些方法的研究分为三个部分：首先，我们研究经典逻辑顺序演算，其术语语言是无递归类型的λ演算。其次，我们研究确定该术语语言的观测相等子集的算法。其中包括一种算法，该算法通过允许某些不是β＆upsi;的β约简，可以提供比β＆upsi; π＆upsi; -equality更好的近似观测近似。 -约简，以及一种通过值限制可扩展性规则确定β＆upsi; π＆upsi; -equality的扩展的算法。第三，我们研究术语语言的βπ统一。因为我们的语言具有多态存在变量和一阶类型函数，所以必须扩展已知的高阶统一过程。而且，与大多数高阶统一版本不同，我们不假设可扩展性规则，因为除非施加值限制，否则它们不会被按值调用语言所约束。

著录项

  • 作者

    Haack, Christian Hauke.;

  • 作者单位

    Kansas State University.;

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

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号