LPF：程序形式化开发中部分函数逻辑的验证和证明的关键

理论计算机科学电子笔记145（2006）3-25www.elsevier.com/locate/entcs程序形式化开发中部分函数的推理Cli B. 琼斯1泰恩河畔纽卡斯尔大学计算机科学学院Newcastle，NE1 7RU，UK摘要部分函数和运算符在程序的形式化开发中被广泛使用，因此开发方法必须阐明如何对它们进行推理。有许多方法掩盖了“一阶谓词演算”不处理未定义逻辑值的事实。还有至少一种特定的“部分函数逻辑”（LPF），它通过使用较弱的逻辑从根本上解决了这个问题。 最近，我们开始意识到LPF适合一种特定的程序开发方式。本文解释了为什么LPF是一个合适的逻辑“验证和证明”的发展关键词：逻辑，部分函数，形式化发展1介绍我想论证的是，经典的有许多方法可以处理部分函数，第4节试图提供一个可以理解替代方案的结构。在研究其他方法之前，让5/ 0 = 1/ 5/ 0/ = 11电子邮件：cliff. ncl.ac.uk1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.10.0024C.B. Jones/Electronic Notes in Theoretical Computer Science 145（2006）3<$i∈Z·fact（i）≥0<$fact（−i）≥0hd[]= 5第一个例子是虽然哈姆雷特说出了一个例子，但这个表达看起来并不令人信服-在关系中嵌入了未定义的算术表达式放弃排中律，我们就得到了一种比FOPC弱的逻辑相反，我愿意把关于事实逻辑的普遍量化的表达式看作是真的：情况是这样的（假设事实是部分的--只在正整数上定义），对于任何i，其中一个析取式是unfined的;但是，由于另一个在那些情况下是真的，所以整个表达式应该是真的。下文表明，试图最终表达式旨在作为一个问题的指针，用一种特定的方法来推理未定义的值（第4.4节指出了它如何成为真）。问题的关键并不在于人们会选择只写这个表达式;但是在从抽象对象的描述中开发程序时，有许多情况会出现像序列或映射上的部分运算符（见第3节）。不久前，我们提出使用我开始意识到LPF非常符合我对开发程序的看法。这句话不应该被理解为我们John Reynolds [38]认为此外，一些全球挑战2正在讨论中：在“程序验证器”3上在IFIP TC2组织的VSTTE工作会议4上，在关于“证明总线”的讨论中，这一点得到了加强1.1一个重要例子许多规范符号允许像图1开头那样定义部分（递归）函数。subp（overpairs）2见http://www.ukcrc.org.uk/gcresearch.pdf3见http://www.fmnet.info/gc6/fm05/4见http://vstte.inf.ethz.ch/index.htmlC.B. Jones/Electronic Notes in Theoretical Computer Science 145（2006）35关于整数）是人为的，以便故意引入偏性问题，在一个足够简单的幌子，梳理出下面的主要问题5函数subp用于计算任意一对整数的i−j，其中i≥j;对于ij，j<$subp（i，j）>0i∈Z·i≥j<$subp（i，j）∈N设i∈Z·i≥j<$subp（i+1，j）/=subp（i，j）等.都需要重新表述，然后才能考虑证据。在以下情况下对算子的重新定义subp（i，j）i−j<$subp（i，j）≥i−j<甚至更不清楚，因为有多种方法可以查看操作符：Xy）最后，必须补充的是，subp示例使本文的讨论集中在关系运算符上;通常，这种方法需要对谓词采取非严格的方法。4.4使所有函数应用程序表示消除术语不能表示的困难的一种方法是坚持所有术语实际上都表示某个东西。如果在术语级处理“非指示”术语的问题由此可见：1≥ 2subp（1， 2）= 1− 2“我的天，“我的天，“我的天，∈B那么，问题当然是subp（1，2）应该表示什么一种方法是回答它表示函数范围内的任意值因此，例如，可以说subp（1， 2）表示任意整数。这确保了蕴涵的后件表示真值-这是真还是假并不重要，因为蕴涵的后件为假的事实确保了蕴涵的整体值为真。这都是标准的FOPC。这种方法在[19，20]中得到了支持，以及Z [45，43]的一些版本。[44][45][46][47][ 48][49][4这种方法的缺点是什么首先，把subp定义为表示最小固定点的解释让subp（1， 2）表示任意值的决定意味着一些20C.B. Jones/Electronic Notes in Theoretical Computer Science 145（2006）3需要子p的图的扩展。这种任意的扩展带来了问题。例如，欠定函数和不确定性之间有一个微妙的区别（参见。[31]）考虑-是否真的是：subp（1， 2）=subp（1， 2）对于实现这些函数的概念，存在着一个含义的泥潭：subp的实现者是否被迫实现令人惊讶的subp（1， 2）=subp（1， 3）+1一些作者因此，先前的定义被替换为（i·：Z|：subp（i，i）= 0）（i·，j：Z |i> j：subp（i，j）= subp（i，j +1）+1）在积极的一面，这一建议有利于一个愉快的证明风格（参见。[20]但它也有自己的问题。放弃递归定义的正常风格可以被视为一个缺点。 此外，接下来的问题是，一般来说，如何识别这种定义中给出的情况。请注意，原始定义-”[10]“故，“”“点）;条件（i>j）在格里斯/施耐德风格必须推导;虽然这是直截了当的在这里，这将是困难的，在许多情况下，一般来说是可以决定的（同样的问题仍然存在于Leavens这种方法与“有序代数”一样，难以定义关于这种方法的后果的进一步警告在[25]中给出：基本上指出，在一种可以定义一个元素类型的规范语言中，范围类型中的“任意结果”的概念似乎会导致无意的过度规范。例如，如果可以定义一个只有一个元素的整数子类（比如5），那么对于这样一个类型的列表，人们可能会被迫得出hd []= 5的结论！5结论我对处理未定义值的偏好--提供适当的工具支持（例如：[21]），推理并不比FOPC更自然C.B. Jones/Electronic Notes in Theoretical Computer Science 145（2006）321正是希望（在各种“大挑战”中在1.2节中有一个暗示，应该可以证明，在那些可以用函数图的隶属关系表示法重新表述的语句和那些使用存在等式的语句之间存在精确的关系Michael Goldsmith在AVoCS上提出了一个问题，指出了一个更有趣的猜想：可以用存在等式写的陈述（在固定重写下）与可以用LPF证明的陈述相同吗？确认1995年7月在康奈尔大学举行的IFIP工作组2.3会议上进行讨论后，提出了一份载有部分内容的文件David Gries和Fred Schneider对于处理未定义值的最佳方式有不同的偏好（与LPF不同）我们的意图是写联合在AVOCS上做特邀演讲的盛情邀请促使我根据“大挑战”辩论重新考虑这些问题9我很感谢与约翰·菲茨杰拉德和迈克尔·戈德史密斯就本文的主题进行了热烈的讨论。我 的 研 究 得 到 了 EPSRC （ 英 国 ） 对 “ 可 靠 性 IRC” （ DIRC - 见www.example.com）和“安全分裂原子”的资助;以及欧盟-IST对“罗丹”的rodin.cs.ncl.ac.uk www.dirc.org.uk引用[1] J. - R. 阿布里尔B-Book：将程序转换为意义。剑桥大学出版社，1996年。[2] R.亚瑟Z中的不确定性：具体化和证明中的问题。 在Farmer等人[15]，第3-12页中。[3] H. 巴林杰Cheng和C.B. 琼斯在程序证明中，覆盖不确定性的一种逻辑Acta Informatica，21：251[4] J. C. Biclinggui，J.S.菲茨杰拉德，宾夕法尼亚州。林赛河Moore，and B.里奇在VDM证明：从业者事实上。Springer-Verlag，1994. ISBN 3-540-19813-X。[5] S.R. 怪我偏值逻辑牛津大学博士论文，1980年。[9]本声明是在IFIP TC2关于“验证软件：理论、工具、实验”的工作会议上打印的22C.B. Jones/Electronic Notes in Theoretical Computer Science 145（2006）3[6] S. 怪我部分逻辑。In D.Gabbay和F.Guenthuer，编者，哲学逻辑手册，第1章。Reidel，1986年。[7] A. 眨眼用于软件规范和验证的三值谓词In R.布鲁姆菲尔德，L. Marshall和R. Jones，editors，VDM-The Way Ahead，pages 243-266. Springer-Verlag，1988.计算机科学笔记，卷。328.[8] J.H. 程 部分函数的逻辑 博士论文，曼彻斯特大学，1986年。[9] J. H. Cheng和C. B. 琼斯 论处理部分函数的逻辑的可用性。在C.摩根和J. C。P. Woodcock，editors，3rd Refinement Workshop，pages 51-69. Springer-Verlag，1991.[10] E. W. 迪杰斯特拉 程序设计的一门学科。 普伦蒂斯-霍尔，1976年。[11] D.德里安科夫走向量化信念的多值逻辑。技术报告192，科学与技术日志中的链接。[12] W.农场主面前.机械化传统方法的部分功能。在Farmer等人[15]，第27[13] S. Finn和M. P·福曼。Lambda系统的逻辑手册。技术报告版本3.2，抽象硬件有限公司，1990年。[14] S.芬恩，M。P. Fourman和J. Longley。在整体设置中的部分功能。Journal of AutomatedReasoning，1996年出版。[15] William Farmer，Manfred Kerber，and Michael Kohlhase，editors.部分功能机械化研讨会论文集，1996年。[16] J. Goguen和J. Meseguer。有序代数I：多重继承、重载、异常和部分操作的等式推导。理论计算机科学，105：217[17] D.格里斯 编程的科学。 Springer-Verlag，1981.[18] RAISE 语言组。RAISE 规范语言。BCS实践者系列。普伦蒂斯·霍尔1992 年ISBN 0-13-752833-7。[19] David Gries和Fred B Schneider。避免因不明确而导致的不确定。Jan van Leeuwen，编辑，Computer Science Today：Recent Trends and Developments，计算机科学讲义第1000卷，第366-373页Springer-Verlag，1995.[20] David Gries和Fred B Schneider。离散数学的逻辑方法。Springer-Verlag，第二版，1996年。[21] C. B.琼斯，K. D.琼斯，宾夕法尼亚州。Lindsay和R.摩尔壁画：一个正式的开发支持系统。Springer-Verlag，1991. ISBN 3-540-19651-X。[22] C.B. 琼斯和CA 米德尔堡 一种经典重构的部分函数的类型逻辑。Acta Informatica，31（5）：399[23] C. B.琼斯正确算法的形式化开发：一个基于Earley识别器的例子在SIGPLAN通告，第7卷第1，第150ACM，1972年1月[24] C. B. 琼斯使用VDM进行系统软件开发。Prentice Hall International，第二版，1990年。ISBN 0-13-880733-7。[25] C.B.琼斯部分函数和逻辑：警告。Information Processing Letters，54（2）：65[26] Manfred Kerber和Michael Kohlhase。不计代价的偏袒。 在Farmer等人[15]，第65[27] S. C.克林 元数学导论。 范·诺斯特拉德1952年