domain-driven-design - 类不变量如何加强前置条件和后置条件？

Question

Link

You can think of the class invariant as a health criterion, which must be fulfilled by all objects in between operations. As a precondition of every public operation of the class, it can therefore be assumed that the class invariant holds. In addition, it can be assumed as a postcondition of every public operation that the class invariant holds. In this sense, the class invariant serves as a general strengthening of both the precondition and the postcondition of public operations in the class. The effective precondition is the formulated precondition in conjunction with the class invariant. Similarly, the effective postcondition is the formulated postcondition in conjunction with the class invariant.

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 上定义了类不变量类(class):

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

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

2. 可以在 Caller 上定义类不变量类(class)以任何方式加强 Foo的先决条件还是后置条件？

3. 如果在 Foo 上定义了类不变量的 cmdIn范围:

a) 如果以 Foo 为前提声明 cmdIn.Length在范围内 1-20 ，但在 Input 上定义的类不变量之一声明 Input.Length应该在范围内 2-19 ，然后 Foo的前提确实加强了？

b) 不是 中的逻辑吗？ a) 有点缺陷，因为如果类不变量已经说明 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 上定义的类不变量之一声明 Output.Length应该在范围内 2-19 ，然后 Foo后置条件确实加强了？

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

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

5. 但我的印象是，引用的文章的意思是说，只要有一个类不变量(即使这个不变量不以任何方式(直接或间接)操作 Foo 的参数和/或返回值，它仍然会加强 Foo 的先决条件和后置条件吗？如果这就是文章实际暗示的内容，那怎么可能？

谢谢

Answer 1

a) Preconditions are typically formulated in terms of the formal parameters of the called operation, so how can class invariant strengthen method's ( Foo's ) preconditions?

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

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. Can class invariant defined on Caller class in any way strengthen Foo's preconditions or postconditions?

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

其余问题的答案从上面逻辑地流动。

嗯。