如果按契约进行设计，除了成员函数的不变量之外，还需要前置条件和后置条件吗？

Question

据我所知，在 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 指出，“当类构造函数完成时、类析构函数开始时、公共成员运行之前以及公共函数完成之后，都会检查不变量。”

谢谢。

Answer 1

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

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

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

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

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

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

Answer 2

是的。

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

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

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

当然，我可能过于简单化了电梯的工作原理。

无论如何，一般来说，前置条件和后置条件作为不变条件是没有意义的； 电梯无需位于 6 楼即可处于有效状态。

可以在这里找到更简洁的示例：拦截和属性：Sasha Goldshtein 的合同设计示例。

Answer 3

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

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

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

当然，在变体中声明布尔项是 true 或 false 有点毫无意义 - 类型系统确保了这一点。