在上下文逻辑程序细化中计算模块
摘要：逻辑程序的细化演算是一种从规范中推导逻辑程序的框架。它基于一个广谱语言，可以表达规范和代码，并通过细化关系来模拟正确实现的概念。本文扩展和推广了以前关于上下文细化的工作。上下文细化通过抽象地捕捉程序的子组件的上下文来简化细化过程，其中通常包括有关自由变量值的信息。本文还扩展和推广了模块细化。模块是一组在公共数据类型上操作的过程的集合；规范模块A与实现模块C之间的模块细化允许将对A的过程的调用系统地替换为对C相应过程的调用。基于模块细化的条件，我们提出了一种从规范模块计算实现模块的方法。在细化演算中，上下文细化和模块细化都被推广自以前的工作，并且结果在一个统一的框架中呈现。
作者：Robert Colvin, Ian J. Hayes and Paul Strooper
论文ID：cs/0608110
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23