逻辑程序的细化微积分
软件工程
2007-05-23 v1 计算机科学中的逻辑
摘要
现有的细化微积分为从规范开发 Imperative 程序提供了框架。本文提出了用于派生逻辑程序的细化微积分。该微积分包含广谱逻辑编程语言，包括可执行构造，如顺序合取、析取和存在量化，以及规范构造，如通用谓词、假设和全称量化。为该广谱语言定义了基于执行的声明式语义。执行是从状态到状态的部分函数，其中状态表示为绑定集合。该语义用于定义程序和规范的意义，包括参数和递归。为完成该微积分，定义了对广谱语言中程序的正确性保护细化概念，并引入了开发程序的细化法则。通过示例演示了该细化微积分，并讨论了原型工具支持。
引用
@article{arxiv.cs/0202002,
title = {A Refinement Calculus for Logic Programs},
author = {Ian Hayes and Robert Colvin and David Hemer and Paul Strooper and Ray Nickson},
journal= {arXiv preprint arXiv:cs/0202002},
year = {2007}
}
备注
36 pages, 3 figures. To be published in Theory and Practice of Logic Programming (TPLP)