3

关联

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

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')前提条件？

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

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

3.如果在's参数上定义了类不变量：FoocmdIn

a) 如果在 range 内的状态的前提条件，但是在应该在 range 内的状态上定义的类不变量之一，那么前提条件确实得到了加强？FoocmdIn.Length1-20InputInput.Length2-19Foo

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

c) 但是如果在应该在 range 内的状态上定义类不变量，那么' 的前提条件不是加强吗？InputInput.Length0-100Foo

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

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

a）如果在 range 内的状态的后置条件，但是在应该在 range 内的状态上定义的类不变量之一，那么的后置条件确实是加强的？FoocmdOut.Length1-20OutputOutput.Length2-19Foo

b）但是如果在应该在 range 内的Output状态上定义不变量，那么' 的后置条件不是加强的吗？Output.Length0-100Foo

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

( _ _ _ _ _ Foo_还是强化Foo的前置条件和后置条件？如果这就是文章的实际含义，那怎么可能？

谢谢

4

1 回答 1

2

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 的前置条件或后置条件？

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

你剩下的问题的答案从上面合乎逻辑地流动。

hth。

于 2013-05-02T22:37:06.227 回答