如果通过合同进行设计，除了成员函数的不变性之外，是否还需要前提条件和后置条件? [英] Are preconditions and postconditions needed in addition to invariants in member functions if doing design by contract?
问题描述
我了解在DbC方法中，先决条件和后置条件附加到一个函数上.
I understand that in the DbC method, preconditions and postconditions are attached to a function.
我想知道的是，这是否同样适用于成员函数.
What I'm wondering is if that applies to member functions as well.
例如，假设我在每个公共函数的末尾使用不变式，则成员函数将如下所示:
For instance, assuming I use invariants at the beginning at end of each public function, a member function will look like this:
(清理我的示例)
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);
}
仅在全局/泛型函数中使用前提条件和后置条件，而只在类内部使用不变式就可以了吗?
Is it okay to use preconditions and postconditions with global/generic functions only and just use invariants inside classes?
这似乎有些矫kill过正，但也许我的例子很糟糕.
This seems like overkill, but maybe its my example is bad.
后置条件不是只检查不变量的子集吗?
Isn't the postcondition just checking a subset of the invariant?
在上面，我正在按照 http://www.digitalmars.com的说明进行操作/ctg/contract.html 指出:在类构造函数完成时，在类析构函数的开头，在运行公共成员之前以及在公共函数完成之后，将检查不变性."
In the above, I am following the instructions of http://www.digitalmars.com/ctg/contract.html that states, "The invariant is checked when a class constructor completes, at the start of the class destructor, before a public member is run, and after a public function finishes."
谢谢.
推荐答案
是.
C类的不变是其所有实例(对象)的共同属性.当且仅当对象处于语义上有效的状态时，该不变变量的值为true.
Class C's invariant is a common property of all of its instances (objects). The invariant evaluates to true if and only if the object is in a semantically valid state.
电梯的不变量可能包含诸如ASSERT(IsStopped() || Door.IsClosed())之类的信息，因为电梯处于不同于停止(例如上升)且门打开的状态是无效的.
An elevator's invariant may contain information such as ASSERT(IsStopped() || Door.IsClosed()), because it is invalid for an elevator to be in a state different than stopped (say, going up) and with the door open.
相反，诸如MoveTo(int flat)的成员函数可能具有CurrentFlat()==flat作为后置条件；因为在调用MoveTo(6)之后，当前平面是6.类似地，它可能具有IsStopped()作为前提，因为(取决于设计)如果不能调用MoveTo函数，电梯已经在移动.首先，您必须查询其状态，确保其已停止，然后调用该函数.
In contrast, a member function such as MoveTo(int flat) may have CurrentFlat()==flat as a postcondition; because after a call to MoveTo(6) the current flat is 6. Similarly, it may have IsStopped() as a precondition, because (depending on the design) you can't invoke function MoveTo if the elevator is already moving. First, you have to query its state, make sure that it is stopped, and then call the function.
当然，我可能会完全简化电梯的工作方式.
Of course I may be totally oversimplifying how an elevator works.
在任何情况下，前置条件和后置条件通常都不会像不变条件那样有意义；电梯不必处于6层即可处于有效状态.
In any case, the preconditions and postconditions will make no sense, in general, as invariant conditions; an elevator doesn't need to be at floor 6 to be in a valid state.
A more concise example can be found here: Interception and Attributes: A Design-By-Contract Sample by Sasha Goldshtein.
这篇关于如果通过合同进行设计，除了成员函数的不变性之外，是否还需要前提条件和后置条件?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
