• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Automated deduction-CADE-16 >Formal metatheory using implicit syntax, and an application to data abstraction for asynchronous systems
【24h】

Formal metatheory using implicit syntax, and an application to data abstraction for asynchronous systems

机译：使用隐式语法的形式元理论及其在异步系统数据抽象中的应用

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

摘要

Abstraction is a useful tool in verification often allowing the proof of correctness of a large and complex system to be reduced to showing the correctness of a much smaller simpler system. We use the Nuprl theorem prover to verify the correctness of a simple but commonly occurring abstraction. From the formal proof, we extract a program that succeeds when the abstraction method is applicable to the concrete input specification and in this case, computes the abstracted system specification. One of the main novelties of our work is our "implicit syntax" approach to formal metatheory of programming languages. Our proof relies entirely on semantic reasoning, and thus aviods the complications that often arise when formally reasoning about syntax. The semantic reasoning contains an implicit construction of the result using inductive predicates over semantic domains that express representability in a particular protocol language. This implicit construction is what allows the synthesis of a program that transforms a concrete specification to an abstract one via recursion on syntax.
机译：抽象是验证的有用工具，通常可以将大型复杂系统的正确性证明简化为显示更小，更简单的系统的正确性。我们使用Nuprl定理证明者来验证简单但经常发生的抽象的正确性。从形式证明中，我们提取了一个程序，当抽象方法适用于具体的输入规范时，该程序将成功，并且在这种情况下，将计算抽象的系统规范。我们工作的主要新颖性之一是我们对编程语言的形式元理论的“隐式语法”方法。我们的证明完全依赖于语义推理，因此避免了在对语法进行形式化推理时经常出现的复杂性。语义推理包含在语义域上使用归纳谓词的结果的隐式构造，这些归纳谓词表示特定协议语言中的可表示性。这种隐式的构造使程序的合成得以实现，该程序通过对语法的递归将具体规范转换为抽象规范。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号