如果通过合同进行设计,除了成员函数中的不变量之外还需要先决条件和后置条件吗？

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

是。

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

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

与此相反，一个成员函数如MoveTo(int flat)可以具有CurrentFlat()==flat作为后置条件 ; 因为通过MoveTo一个呼叫后（6）的当前平是6类似地，它可以具有IsStopped()作为一个先决条件，因为（根据设计），则可以不调用函数通过MoveTo如果电梯已经移动，。首先，您必须查询其状态，确保其已停止，然后调用该函数。

当然，我可能会完全简化电梯的工作方式。

在任何情况下，前提条件和后置条件通常都不会像不变条件那样有意义；电梯不必处于6层即可处于有效状态。

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

Answer 2

将类中的合同限制为不变量并非最佳.

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

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

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

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

后置条件正在试图该方法满足其义务后置条件也是不变量的补充.当然,对象的状态必须在方法执行后保持一致,但后置条件检查是否执行了预期的操作(即list.add(i)应该具有list.has(i)为真的结果和list.count = old list.count + 1).