类不变量如何加强前置条件和后置条件？

Question

Link

您可以将类不变量视为健康标准，它必须 由操作之间的所有对象实现。作为前提 对于该类的每个公共操作，因此可以假设 类不变量成立。此外，可以假设为 类不变的每个公共操作的后置条件 持有。在这个意义上，类不变量作为一般 强化前置条件和后置条件 类中的公共操作。有效的前提是 与类不变量一起制定前提条件。 同样，有效的后置条件是 后置条件与类不变量相结合。

public class Server
{
     // other code ommited
    public Output Foo(Input cmdIn)
    {
        ...
        return cmdOut;
    }
}


public class Caller
{  
    // other code ommited

    /* calls Server.Foo */
    public void Call()
    {...}
}

public class Input
{
    // other code ommited

    public int Length
    {...}
}

public class Output
{
    // other code ommited

    public int Length
    {...}
}

1.如果类不变量在Server类上定义：

a) 前置条件通常是根据被调用操作的形式参数来制定的，那么类不变量如何加强方法的（Foo's）前提条件？

b) 后置条件是根据被调用方法的返回值制定的，那么类不变量如何加强方法的（Foo的) 后置条件？

2. 定义在Caller 类上的类不变量 能否以任何方式加强Foo 的前置条件 或后置条件？

3.如果在Foo的cmdIn参数上定义了类不变量：

a) 如果Foo 上的前提条件 表明cmdIn.Length 在1-20 范围内，但Input 上定义的类不变量之一 表明@ 987654334@ 应该在2-19 范围内，那么Foo 的前置条件 确实加强了？

b) a) 中的逻辑是不是有点缺陷，因为如果 class invariant 已经声明 Input.Length 应该在 2-19 范围内，是那么Foo 定义一个并不总是true（cmdIn.Length 不能保存值1 或20）的前提条件 是错误的

c) 但是如果在Input 上定义的类不变量 声明Input.Length 应该在0-100 范围内，那么Foo 的前置条件 是'加强吗？

d) 在cmdIn 上定义的类不变量 是否也能以某种方式加强Foo 的后置条件？

4.如果类不变量定义在Foo的返回值

a) 如果Foo 上的后置条件 表明cmdOut.Length 在1-20 范围内，但Output 上定义的类不变量之一 表明@ 987654355@应该在2-19的范围内，那么Foo的后置条件确实是加强了？

b) 但是如果Output 上定义的不变量声明Output.Length 应该在0-100 范围内，那么Foo 的后置条件 没有加强？

c) 在Output 上定义的类不变量 是否也能以某种方式加强Foo 的前提条件？

5. 但我得到的印象是，引用文章的意思是说，仅通过具有 类不变量（即使这个 不变量不会以任何方式（直接或间接）对Foo 的参数和/或返回值进行操作，它仍会加强Foo 的前置条件 和后置条件？如果这就是文章的实际含义，那怎么可能？

谢谢

Answer 1

a) 前提条件通常以形式表述 被调用操作的参数，那么如何类不变量 加强方法（Foo's）的前置条件？

我怀疑这是造成您误解的关键。前置条件可能包括形式参数——但不限于它们。他们可以——而且经常这样做——也指类特征（属性/操作）。通常，不变量和前置条件的组合定义了一组约束条件，在调用时操作必须满足其后置条件之前必须满足这些约束条件。类似地，操作必须保证在完成时满足其后置条件和任何不变量。以有界缓冲区为例：

Class BoundedBuffer<T> {
   public int max    // max #items the buffer can hold
   public int count  // how many items currently in the buffer

   void push(T item) {...}
   T    pop() {...}
}

push() 的前提条件是缓冲区尚未达到其最大大小：

 pre: count < max

所以这里的前置条件甚至没有提到操作的形参。我们还可以为 Buffer 声明一个不变量：

inv: count >=0  //can't have -ve number of elements in the buffer

它加强了前置条件，因为它意味着在push() 操作必须满足其后置条件之前必须为真。这两个子句在逻辑上是与在一起的。所以有效的前置条件是count >=0 AND count < max。这是一个比单独的前置条件更强（更严格）的约束。

请注意，该概念不限于前置条件指类特征的情况。让我们添加一个约束，即添加到缓冲区的任何单个项目的大小必须小于某个上限：

pre: count < max AND item.size() <= MAX_ITEM_SIZE

添加不变量仍将有效前置条件增强为：

pre: count < max AND item.size() <= MAX_ITEM_SIZE AND count >=0

总而言之：在调用操作之前和操作完成之后，不变量必须保持不变。因此，它们都加强了两者。

1. 在 Caller 类上定义的类不变量能否以任何方式加强 Foo 的前置条件或后置条件？

没有。不变量仅适用于定义它们的类。

您剩余问题的答案从上面按逻辑顺序排列。

第一次。