精化中的明晰性与粒度
软件工程
2011-06-22 v1
摘要
本文重新审视了在具体层面引入抽象层面所没有的动作的精化。它区分了在抽象层面“明晰可见”的具体动作，以及不同抽象层次之间动作粒度的变化。本文的主要贡献在于探索这些不同的“动作精化”方法与所使用的基本精化关系之间的关联。特别地，它展示了“精化 skip”方法与基于失败的精化关系不相容，并因此揭示了 Event-B 精化设计中的一些决策是相互纠缠的。
引用
@article{arxiv.1106.4099,
title = {Perspicuity and Granularity in Refinement},
author = {Eerke Boiten},
journal= {arXiv preprint arXiv:1106.4099},
year = {2011}
}
备注
In Proceedings Refine 2011, arXiv:1106.3488