接口不变的时间逻辑

Question

我正在寻找某种时间逻辑，用于在接口中表达不变性。由于接口未指定数据表示，因此不变性必须仅依靠接口的公开功能。

例如，假设我们有一个简单的界面（Java样式）总和：

interface Sum {
    public void add (int a);
    public int getSum();
}

我想在一个不变的情况下表达 getSum 返回总和 a 在所有电话中 add(a), ，不使用此总和的任何数据表示。

我能想到的唯一方法是使用某种形式的时间逻辑。我可以阅读有关此主题的文献吗？任何指针都将不胜感激。

Answer 1

标准方法是使用所谓的 幽灵变量. 。幽灵变量就像一个普通变量一样，只是仅出现在规范中（它不是程序实际执行的一部分）。换句话说，原始程序中不存在幽灵变量。它由规格添加。前提条件，后条件和不变性被允许参考幽灵变量。

直观地，幽灵变量使您可以保持有关过去曾经调用过哪些方法的状态；这些方法的规格可以更新幽灵变量，从而记住此信息。

我们可以通过添加幽灵变量来解决您的特定挑战问题 totalSoFar. 。然后，我们为每种方法添加了适当的规范，例如：

interface Sum {
    ghost int totalSoFar = 0;

    /* postcondition: totalSoFar = old(totalSoFar) + a */
    public void add (int a);

    /* postcondition: returnvalue = totalSoFar */
    public int getSum();
}

注意如何后解决方案 add() 根据传递给的参数更新幽灵变量 add(). 。同样，后期 getSum() 描述了其幽灵变量的返回值。

这是标准模式：您使用幽灵变量来跟踪所需的任何状态；对于修改此状态的方法，您可以编写后条件以更新幽灵变量中的状态；对于Getters，您就幽灵变量的状态表达了他们的结果。

Answer 2

无论您做什么，您的规范都将具有内部状态反映对象内部的累加器。对于这个简单的课程，规范不会比实现更简单。关键是，对于更复杂的情况，规范更简单。考虑一个词典，您可以在键下添加数据，并且必须以后能够检索。您的规范很可能等效于键/值对的线性阵列，并且搜索简单的线性搜索。您的实施也许是基于哈希或平衡二进制树的计划。这 规格 很容易推理，您证明了您的 执行 行为与规范相同，您将设置。明天，您将剥夺实施方式，并用一些奇特的结构替换，再次证明它符合规范。在其他地方没有变化。

规格本质上是在另一种（希望更容易处理的）编程语言中再次编写相同的程序，可能已经预言了任何性能注意事项，并提出两个程序都可以做到这一点。规格语言最新的 很多 比常规编程语言更难使用（规格也可能有错误...），而且证明它们的行为同样的证据并不是对胆小者的胆怯。而且，如果我想出一个关于我的程序应如何行为的想法，并对此进行编程，则可以说规范和最终程序将共享相同的误解和错过的角落案例。 “程序验证”运动已经出现了巨大的失败。看看贝瑞的“软件工程学科的学术合法性”（CMU/SEI-92-TR-34），以示例为几十行的程序，书面并“证明正确”，然后固定并再次验证 在学术期刊上出版 由该地区的一些最大专家多次，这是错误的。