- 冒号空间 - https://blog.zhenghui.org -

Reply To: class invariant

invariant的确只是保证对象的状态约束的。如果超出内部状态储存的范围,而(部分地)依赖外部状态,那就便不是invariant。事实上,这也超出了该类的能力。比如,依赖传入参数,那就是postcondition的责任。

其实,你举的这个例子可以用invariant或postcondition保证。首先,Pair的constructor的postcondition一定会保证Pair(x, y).Left() == x, Pair(x, y).Right() == y。如果Pair被设计为immutable的,那么它需要保证所有的public方法保持left/right不变(在C++中可以在这些方法签名的最后加上const);如果是mutable的,那么在所有的mutator的postcondition中应明确规范新的left或right应满足的条件(但这时的left/right不一定是当初从constructor中传入的x/y)。

另外,DbC机制应当能自动生成检验invariant的测试用例。


Share