冒号论坛

1. 

   Todd
   Member

   wikipedia上class invaraint的定义：
   In computer programming, specifically object-oriented programming, a class invariant is an invariant used to constrain objects of a class. Methods of the class should preserve the invariant. The class invariant constrains the state stored in the object.Class invariants are established during construction and constantly maintained between calls to public methods. Temporary breaking of class invariance between private method calls is possible, although not encouraged.

   这个定义以及后面的几个例子中的invariant是针对状态的，比如：Date类的month属性是1到12的整数。而我认为这里忽略了一种非状态的class invariant，比如：Pair类应该有这样的invariant：

   Pair(x, y).Left() == x, Pair(x, y).Right() == y

   其中，Pair()是Pair类的构造函数，Left()，Right()分别是取左、右值。这种非状态的，描述抽象数据类型构造和使用关系整体规范的class invariant似乎无法通过在类内部通过进行状态检查来保证，而单元测试时则应该明确并重点测试这样的invariant。

   Posted 1 year ago #
2. 

   hui
   Key Master

   invariant的确只是保证对象的状态约束的。如果超出内部状态储存的范围，而（部分地）依赖外部状态，那就便不是invariant。事实上，这也超出了该类的能力。比如，依赖传入参数，那就是postcondition的责任。
   其实，你举的这个例子可以用invariant或postcondition保证。首先，Pair的constructor的postcondition一定会保证Pair(x, y).Left() == x, Pair(x, y).Right() == y。如果Pair被设计为immutable的，那么它需要保证所有的public方法保持left/right不变（在Ｃ++中可以在这些方法签名的最后加上const）；如果是mutable的，那么在所有的mutator的postcondition中应明确规范新的left或right应满足的条件（但这时的left/right不一定是当初从constructor中传入的x/y）。
   另外，DbC机制应当能自动生成检验invariant的测试用例。

   Posted 1 year ago #
3. 

   Todd
   Member

   上面例子中的Pair(x, y).Left() == x, Pair(x, y).Right() == y的确可以作为构造函数的postcondition。不过，我这里主要想表达的意思是class invariant这个术语更适合用于表达一种整体上的类特征，除了上面pair的例子，stack的invariant是LIFO，queue的invariant是FIFO。

   Posted 1 year ago #
4. 

   hui
   Key Master

   无论是否为整体类特征，都应可以通过类内部的状态来检验的（你提到的stack和queue的invariant也不例外），否则又如何判定invariant是否被破坏呢？如果还依赖外部context的话，那便不是invariant了。当然，如果一个类的invariant在理论上非常复杂，难以用常规的statement来表示，那么只能退而求其次，采用弱化的invariant来简化，然后辅以单元测试。

   Posted 1 year ago #
5. 

   Todd
   Member

   >>如果还依赖外部context的话，那便不是invariant了。

   我不知道Pair(x, y).Left() == x, Pair(x, y).Right() == y这样的invariant是否算作对外部context的依赖。我认为这是类对外部输入进行的“变换”，变换之间保持了某种不变。我认为class invariant应该强调的是各个public方法之间的关系，比如：对于stack类孤立地测试（或保证）push方法，并检查内部状态是不可取的，而应该从外部测试（或保证）push和pop之间保持的LIFO invariant。所以，更具体地说，我认为class invariant应该强调类的特征，即公有方法间所保持的某种不变性。基于内部状态检查class invariant的方式可以达到目的，但是我认为没有抓住class invariant的本质。

   Posted 1 year ago #
6. 

   hui
   Key Master

   >>我认为class invariant应该强调的是各个public方法之间的关系
   不是，class invariant强调的是一个类的任何对象都应时时处于一个正常/合法的状态中。之所以提到public方法，是因为客户只有通过它才有可能破坏这个invariant（当然前提是constructor的postcondition满足这个invariant）。

   你提到的LIFO是Stack的一个类级别规范（你所说的整体规范应当指的就是这个吧），但该规范只能通过push/pop/pushAll/popAll等具体API的precondition/postcondition来体现。换言之，class invariant是类级别规范的一部分，但不是全部。或者说，class invariant的成立对于保证一个类的行为正确性来说，是一个必要但不充分的条件。你正确意识到了有些规范具有整体性，不能孤立地只看某个public方法，但却把类级别规范与class invariant混同了。

   Posted 1 year ago #
7. 

   Todd
   Member

   >>class invariant强调的是一个类的任何对象都应时时处于一个正常/合法的状态中
   是的，wikipedia也是这个意思。用class invariant这个术语表达对象状态的正常/合法有点儿可惜，我更喜欢：
   对象状态正常/合法-> class validation
   类级别规范-> class invariant

   Posted 1 year ago #
8. 

   hui
   Key Master

   可以这么来理解class invariant：它是附加在每个public方法之上的precondition和postcondition。倒过来看，对所有public方法中同时为precondition和postcondition的predicate提取公因式，便得到class invariant。

   Posted 1 year ago #

RSS feed for this topic

Reply

You must log in to post.