被前置或后置需要在除成员函数不变量，如果合同在做设计？(Are preconditions and

据我所知，在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类的不变是它的所有实例（对象）的共同财产。不变的计算结果为真当且仅当对象是在语义上有效状态。

电梯的不变可能包含的信息，如ASSERT(IsStopped() || Door.IsClosed())因为它是无效的电梯是在比停止不同的状态（比如，往上走），并与门打开。

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

当然，我可能完全简单化的电梯是如何工作的。

在任何情况下，前置或后置将是毫无意义的，在一般情况下，不变的条件; 电梯并不需要在6楼是处于有效状态。

更简洁的例子可以在这里找到：拦截和属性：设计按合同样本萨沙Goldshtein 。

Answer 2:

限制在类合同不变量是不是最佳的。

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

不变，前提条件和后置条件有非常不同的角色。

不变量确认对象的内部一致性。 他们应该在构造函数的末尾，在每次方法调用后有效。

预条件检查对象的状态和参数是适合于该方法的执行。 前提条件是不变量的补充。它们涵盖的参数（更强检查该类型本身，即不为空，> 0，...等）的检查，但也可以检查对象内部状态（即调用file.write（“你好”）是一个有效的电话只有file.is_rw和file.is_open是真实的）。

后置条件是cheking，该方法满足其义务后置条件也对不变量的补充。当然，对象的状态必须是方法执行前后连贯，但事后条件所检查的执行预期的动作（即list.add（我）应该有作为的后果是list.has（i）为真和list.count =旧list.count + 1）。

Answer 3:

好了，不变的一点是，它描述的东西， 在任何时间对象的真实 。在这种情况下，事情是在烤架上，或不（以之间没有任何东西）。他们通常描述对象的整个状态的属性。

前置和后置条件描述事情是真的只是一个方法之前执行，只是后，并会关注这一点应该已经感动方法的状态 。这是不同的，据推测，从物体的状态。前置和后置条件可能会被认为是描述方法的足迹 - 它需要的正是，正是它感动。

所以，到了具体问题，想法做不同的事情，所以你可能想都。你当然不能只用不变量，而不是前置和后置条件 - 在这种情况下，目标不变的部分是“东西是在烤架上或不”，但lightOnFire的前提需要知道该项目是在烤架上。你永远不能从对象不变推断出这一点。这是事实，从前期和后置条件和已知的启动状态，你可以（假设对象结构只有通过方法可变的，前置和后置条件描述了所有环境变化），推断对象不变。然而，这可能是复杂的，而当你陈述的事情“语言”，它更容易只是提供两种。

当然，在该国一个布尔项目变种做的是真或假是有点无意义 - 该型系统可以保证。

文章来源: Are preconditions and postconditions needed in addition to invariants in member functions if doing design by contract?