On the Frame Problem in Procedure Specifications
On the Frame Problem in Procedure Specifications
复制标题
论程序规范中的框架问题
DOI：
--
复制
发表时间：
1995
期刊：
影响因子：
--
通讯作者：
R. Reiter
中科院分区：
文献类型：
--
作者：
Alexander Borgida;J. Mylopoulos;R. Reiter
本文提供了标准前置/后置条件风格的过程的形式规范变得冗长、繁琐和难以更改的情况的例子，这一问题在具有继承的面向对象规范的情况下尤其严重。我们将问题确定为不能表示过程只更改了它必须更改的那些内容，而其他所有内容都保持不变，并回顾了软件规范社区中处理此“框架问题”的一些尝试。论文的第二部分采用了最近提出的一项解决人工智能框架问题的建议--解释闭包公理的概念--以提供一种方法，通过这种方法，人们可以简洁而模块化地陈述这种条件，另外一个好处是，可以提醒说明者注意她在过程规范中可能遗漏的内容。由于此方法基于标准谓词逻辑，因此其语义相对简单。文中还提出了一种算法，该算法可以从前置/后置条件规范中生成语法上的解释闭包公理，只要它们是用受限语言编写的；它还提出了一个支持它的模型理论。>；
The paper provides examples of situations where formal specifications of procedures in the standard pre/postcondition style become lengthy, cumbersome and difficult to change, a problem which is particularly acute in the case of object oriented specifications with inheritance. We identify the problem as the inability to express that a procedure changes only those things it has to, leaving everything else unmodified, and review some attempts at dealing with this "frame problem" in the software specification community. The second part of the paper adapts a recent proposal for a solution to the frame problem in artificial intelligence-the notion of explanation closure axioms-to provide an approach whereby one can state such conditions succinctly and modularly, with the added advantage of having the specifier be reminded of things that she may have omitted saying in procedure specifications. Since this approach is based on standard predicate logic, its semantics are relatively straightforward. The paper also suggests an algorithm which generates syntactically the explanation closure axioms from the pre/postcondition specifications, provided they are written in a restricted language; it also suggests a model theory supporting it. >