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

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.如果类不变量是在Server类上定义的：

a( 预条件通常是根据被调用操作的形式参数来制定的，那么类不变量如何加强方法(Foo’s(的先决条件

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

2.在Caller类上定义的类不变量是否可以以任何方式增强Foo的preconditions或后条件？

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

a( 如果Foo上的前提条件声明cmdIn.Length在范围1-20内，但Input上定义的class不变量之一声明Input.Length应该在范围2-19内，那么Foo的1前提条件确实被强化了？

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

c( 但是，如果在Input上定义的类不变量声明Input.Length应该在0-100的范围内，那么Foo的precondition不是加强的？

d( cmdIn上定义的类不变量是否也能以某种方式加强Foo的postcondition？

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

a( 如果Foo上的后条件声明cmdOut.Length在范围1-20内，但在Output上定义的class不变量之一声明Output.Length应该在范围2-19内，那么Foo的<em]后条件>确实是加强的？

b( 但如果定义在Output上的不变量表明Output.Length应该在0-100的范围内，那么Foo的后条件就没有增强？

c( 在Output上定义的类不变量是否也能以某种方式加强Foo的precondition？

5.但我的印象是，引用的文章的意思是，只要有一个类不变量(即使这个不变量决条件和后决条件？如果这就是文章的真正含义，那怎么可能呢？

感谢

Answer 1

a( 先决条件通常是根据形式被调用操作的参数，那么类如何保持不变强化方法的前提条件？

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

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

所以这里的前置条件甚至没有提到运算的形式参数。我们还可以为缓冲区声明一个不变量：

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。