首页> 外文期刊>Journal of logic and computation >A Verification Logic for Rewriting Logic
【24h】

A Verification Logic for Rewriting Logic

机译:用于重写逻辑的验证逻辑

获取原文
获取原文并翻译 | 示例

摘要

This paper proposes the development of a logic for verifying properties of programs in rewriting logic. Rewriting logic is primarily a logic of change, in which deduction corresponds directly to computation, and not a logic to talk about change in a more indirect and global manner, such as the different modal and temporal logics that can be found in the literature. We start by defining a modal action logic (VLRL) in which rewrite rules are captured as actions. The main novelty of this logic is a topological modality associated with state constructors that allows us to reason about the structure of states, stating that the current state can be decomposed into regions satisfying certain properties. Then, on top of the modal logic, we define a temporal logic for reasoning about properties of the computations generated from rewrite theories, and demonstrate its potential by means of several examples.
机译:本文提出了一种用于在重写逻辑中验证程序属性的逻辑的开发。重写逻辑主要是变化的逻辑,其中的推论直接对应于计算,而不是以更间接和全局的方式谈论变化的逻辑,例如可以在文献中找到的不同的模态和时间逻辑。我们首先定义一个模式动作逻辑(VLRL),在该模式中,重写规则被捕获为动作。该逻辑的主要新颖之处在于与状态构造函数关联的拓扑模态,该拓扑模态允许我们对状态的结构进行推理,指出当前状态可以分解为满足某些属性的区域。然后,在模态逻辑的基础上,我们定义了一个时间逻辑,用于推理由重写理论生成的计算的属性,并通过几个示例展示其潜力。

著录项

相似文献

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

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号