A logic covering undefinedness in program proofs
A logic covering undefinedness in program proofs
复制标题
DOI：
10.1007/bf00264250
复制
发表时间：
1984-10
期刊：
影响因子：
0.6
通讯作者：
H. Barringer;J. H. Cheng;Cliff B. Jones
中科院分区：
文献类型：
--
作者：
H. Barringer;J. H. Cheng;Cliff B. Jones
递归定义经常导致部分函数;迭代产生的程序可能无法终止某些输入。关于这些函数或程序的证明应该在反映“未定义值”的可能性的逻辑系统中进行。本文提供了这样一个逻辑的公理化及其使用的例子。
Recursive definition often results in partial functions; iteration gives rise to programs which may fail to terminate for some imputs. Proofs about such functions or programs should be conducted in logical systems which reflect the possibility of “undefined values”. This paper provides an axiomatization of such a logic together with examples of its use.