• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International Conference on Logic for Programming, Artificial Intelligence, and Reasoning(LPAR 2005); 20051202-06; Montego Bay(JM) >Automatic Validation of Transformation Rules for Java Verification Against a Rewriting Semantics
【24h】

Automatic Validation of Transformation Rules for Java Verification Against a Rewriting Semantics

机译：针对重写语义的Java验证的转换规则的自动验证

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

摘要

This paper presents a methodology for automatically validating program transformation rules that are part of a calculus for Java source code verification. We target the Java Dynamic Logic calculus which is implemented in the interactive prover of the KeY system. As a basis for validation, we take an existing SOS style rewriting logic semantics for Java, formalized in the input language of the Maude system. That semantics is 'lifted' to cope with schematic programs like the ones appearing in program transformation rules. The rewriting theory is further extended to generate valid initial states for involved program fragments, and to check the final states for equivalence. The result is used in frequent validation runs over the relevant fragment of the calculus in the KeY system.
机译：本文提出了一种自动验证程序转换规则的方法，该方法是Java源代码验证演算的一部分。我们针对在KeY系统的交互式证明程序中实现的Java动态逻辑演算。作为验证的基础，我们采用了Java的现有SOS样式重写逻辑语义，并以Maude系统的输入语言形式化。语义被“提升”以应付示意图程序，例如程序转换规则中出现的程序。重写理论进一步得到扩展，可以为所涉及的程序片段生成有效的初始状态，并检查最终状态的等效性。该结果用于KeY系统中微积分的相关片段的频繁验证运行。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号