4

我知道在 DbC 方法中，前置条件和后置条件附加到一个函数。

我想知道这是否也适用于成员函数。

例如，假设我在每个公共函数的开头使用不变量，成员函数将如下所示：

编辑：（清理我的例子）

void Charcoal::LightOnFire() {
  invariant();
  in_LightOnFire();

  StartBurning();    
  m_Status = STATUS_BURNING;
  m_Color = 0xCCCCCC;

  return; // last return in body

  out_LightOnFire();
  invariant();
}

inline void Charcoal::in_LightOnFire() {
  #ifndef _RELEASE_
  assert (m_Status == STATUS_UNLIT);
  assert (m_OnTheGrill == true);
  assert (m_DousedInLighterFluid == true);
  #endif
}

inline void Charcoal::out_LightOnFire() {
  #ifndef _RELEASE_
  assert(m_Status == STATUS_BURNING);
  assert(m_Color == 0xCCCCCC);
  #endif
}

// class invariant
inline void Charcoal::invariant() {
  assert(m_Status == STATUS_UNLIT || m_Status == STATUS_BURNING || m_Status == STATUS_ASHY);
  assert(m_Color == 0x000000 || m_Color == 0xCCCCCC || m_Color == 0xEEEEEE);
}

是否可以仅对全局/泛型函数使用前置条件和后置条件，而只在类中使用不变量？

这似乎有点矫枉过正，但也许我的例子很糟糕。

编辑：

后置条件不只是检查不变量的子集吗？

在上面，我遵循http://www.digitalmars.com/ctg/contract.html的说明，其中指出：“当类构造函数完成时，在类析构函数的开始，在公共之前检查不变量成员运行，并且在公共函数完成后。”

谢谢。

4

3 回答 3

5

是的。

C 类的不变量是其所有实例（对象）的共同属性。当且仅当对象处于语义上有效的状态时，不变量的计算结果为 true。

电梯的不变量可能包含诸如 之类的信息ASSERT(IsStopped() || Door.IsClosed())，因为电梯处于与停止（例如，上升）不同的状态并且门打开是无效的。

相比之下，成员函数如MoveTo(int flat)可能有CurrentFlat()==flat作为后置条件；因为在调用 MoveTo(6) 之后，当前平面为 6。同样，它可能具有IsStopped()作为前提条件，因为（取决于设计）如果电梯已经在移动，则不能调用函数 MoveTo。首先，您必须查询它的状态，确保它已停止，然后调用该函数。

当然，我可能完全过分简化了电梯的工作原理。

在任何情况下，前置条件和后置条件作为不变条件通常是没有意义的；电梯不需要在 6 楼处于有效状态。

可以在此处找到更简洁的示例：Interception and Attributes: A Design-By-Contract Sample by Sasha Goldshtein。

于 2009-08-04T13:31:24.680 回答
5

将类中的契约限制为不变量并不是最优的。

前置条件和后置条件不仅仅是不变量的一个子集。

不变量、前置条件和后置条件具有非常不同的作用。

不变量确认了对象的内部连贯性。它们应该在构造函数的末尾以及每个方法调用之前和之后都有效。

前提条件是检查对象的状态和参数是否适合方法的执行。先决条件是对不变量的补充。它们涵盖了参数的检查（对类型本身的更强检查，即不为空，> 0，.. 等），但也可以检查对象的内部状态（即对 file.write( "hello" ) 的调用是仅当 file.is_rw 和 file.is_open 为真时才有效调用）。

后置条件检查方法是否满足其义务后置条件也是对不变量的补充。当然，在方法执行之后对象的状态必须是一致的，但是后置条件正在检查是否执行了预期的操作（即 list.add(i) 应该因此 list.has(i) 为真和 list.count = 旧 list.count + 1)。

于 2009-09-19T21:27:15.753 回答
2

嗯，不变量的意义在于它描述了对象在任何时候都是真实的东西。在这种情况下，烤架上有东西，或者没有（两者之间没有）。它们通常描述对象整个状态的属性。

前置条件和后置条件描述了在方法执行之前和之后为真的事物，并且只涉及该方法应该触及的状态。这可能与对象的状态不同。前置条件和后置条件可能被认为是描述方法的足迹——正是它需要什么，它触及了什么。

所以，对于具体的问题，这些想法做不同的事情，所以你很可能两者都想要。你当然不能只使用不变量而不是前置条件和后置条件——在这种情况下，对象不变量的一部分是“某物是否在烤架上”，但 lightOnFire 的前提条件需要知道该物品在烤架上。您永远无法从对象不变量中推断出这一点。确实，从前置条件和后置条件以及已知的起始状态，您可以（假设对象结构仅通过方法是可变的，并且前置条件和后置条件描述了所有环境变化），推断出对象不变量。但是，这可能很复杂，当您“用语言”陈述事物时，两者都提供会更容易。

当然，在变体中声明布尔项是真还是假有点没有意义——类型系统可以确保这一点。

于 2009-08-02T20:17:13.350 回答