• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Science of Computer Programming >Mechanical reasoning about families of UTP theories
【24h】

Mechanical reasoning about families of UTP theories

机译：关于UTP理论族的机械推理

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

摘要

The Unifying Theories of Programming (UTP) of Hoare and He is a general framework in which the semantics of a variety of specification and programming languages can be uniformly defined. In this paper we present a semantic embedding of the UTP into the ProofPower-Z theorem prover; it concisely captures the notion of UTP theory, theory in stantiation, and, additionally, type restrictions on the alphabet of UTP predicates. We show how the encoding can be used to reason about UTP theories and their predicates, includ ing models of particular specifications and programs. We support encoding and reasoning about combinations of predicates of various theory instantiations, as typically found in UTP models. Our results go beyond what has already been discussed in the literature in that we support encoding of both theories and programs (or their specifications), and high-level proof tactics. We also create structuring mechanisms that support the incremental con struction and reuse of encoded theories, associated laws and proof tactics.
机译：Hoare and He的统一编程理论（UTP）是一个通用框架，可以在其中统一定义各种规范和编程语言的语义。在本文中，我们提出了UTP到ProofPower-Z定理证明者的语义嵌入。它简明地记录了UTP理论的概念，实例化的理论，以及对UTP谓词字母的类型限制。我们将展示如何使用编码来推理UTP理论及其谓词，包括特定规范和程序的模型。我们支持各种理论实例的谓词组合的编码和推理，这通常在UTP模型中可以找到。我们的结果超出了文献中已讨论的范围，因为我们支持理论和程序（或其规范）以及高级证明策略的编码。我们还创建了结构化机制，以支持编码理论，相关法律和证明策略的增量构建和重用。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号