通过自动理论形成发现不变量
计算机科学中的逻辑
2011-06-22 v1 人工智能
软件工程
摘要
精化是掌控形式化系统建模时所产生复杂性的强大机制。精化也带来了额外的证明义务——要求开发者发现与其设计决策相关的性质。为了减轻这一负担，我们研究了如何将通用理论形成工具 HR 用于在 Event-B 语境下自动发现此类性质。在此，我们开发了一种启发式方法以实现不变量的自动发现，并报告了为评估该方法而进行的一系列实验。所开发的启发式集合为针对特定 Event-B 开发定制 HR 提供了系统性指导。这些启发式基于证明失败分析，并已产生了一些有前景的结果。
引用
@article{arxiv.1106.4090,
title = {Discovery of Invariants through Automated Theory Formation},
author = {Maria Teresa Llano and Andrew Ireland and Alison Pease},
journal= {arXiv preprint arXiv:1106.4090},
year = {2011}
}
备注
In Proceedings Refine 2011, arXiv:1106.3488