类不变如何强化前后条件？

Question

链接

您可以将类不变量视为一个健康标准，操作之间的所有对象都必须满足该标准。作为类的每个公共操作的先决条件，因此可以假设类不变量成立。此外，可以假设它是类不变量所持有的每个公共操作的后条件。从这个意义上说，类不变量是对类中公共操作的先决条件和后决条件的一般强化。有效的前提条件是与类不变量相结合的公式化的前提条件。类似地，有效后条件是与类不变量结合的公式化后条件。

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.如果在服务器上定义了类不变量类：

a） 先决条件通常是根据被调用操作的形式参数来表示的，所以类不变量如何加强方法的（Foo）先决条件呢？

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

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

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

a）如果Foo上的先决条件指出cmdIn。长度在范围1-20内，但是在Input上定义的类不变量之一声明Input。长度应该在2-19的范围内，那么Foo的先决条件确实是加强的？

b） a）中的逻辑不是有点缺陷吗，因为if类不变量已经声明了输入。长度应该在范围2-19内，那么Foo定义一个不总是true（cmdIn.Length不能保存值1或20）的前提条件不是一个错误吗

c）但如果类不变量上定义的输入状态，输入。长度应该在0-100范围内，那么Foo的前提条件不是加强吗？

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

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

a） 如果Foo上的后置条件表明cmdOut。长度在范围1-20内，但在Output上定义的一个类不变量表示Output。长度应该在2-19范围内，那么Foo的后置条件确实加强了吗？

b）但如果Output上定义的不变量表示Output。长度应该在0-100范围内，那么Foo的后置没有加强？

c） 在Output上定义的类不变量也能以某种方式增强Foo的前提条件吗？

5.但我得到的印象是，引用的文章的意思是，只要有一个类不变量（即使这个不变量不以任何方式（直接或间接）对Foo的参数和/或返回值进行操作），它仍然会加强Foo的先决条件和后决条件？如果这就是文章的真正含义，那怎么可能呢？

谢谢




Answer 1

a） 先决条件通常是根据被调用操作的形式参数来表示的，所以类不变量如何加强方法（Foo）的先决条件呢？

我怀疑这是你误解的关键。先决条件可以包括形式参数，但不限于它们。它们也可以（而且经常这样做）引用类特性（属性/操作）。一般来说，不变量和前置条件的组合定义了一组约束，在操作被调用时必须满足其后置条件之前，这些约束必须得到满足。同样，操作必须保证在完成时满足其后置条件和任何不变量。以有界缓冲区为例：

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

它加强了前提条件，因为它包含了在ush（）操作必须满足其后条件之前必须为真的内容。这两个从句在逻辑上结合在一起。所以有效的前提条件是计数

注意，这个概念并不局限于前置条件引用类特性的情况。让我们添加一个约束，即添加到缓冲区的任何单个项的大小必须小于某个上限：

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

添加不变量仍然会加强有效的先决条件，使其成为：

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

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

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

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

你剩下的问题的答案顺理成章地从上面流下来。

嗯。