java - 如何在java中识别类中的不变量？

Question

我了解什么是 Invariant，但我遇到的问题是从一个类中识别它。生病解释-当课堂上的老师向我们展示Java代码并询问我们什么是不变量时-这是我掉下来的时候，我不知道要识别它。

再次 - 我知道它是什么 - 只是很难识别它。如果你能解释或给我提示如何做，我很高兴听到。谢谢你。

编辑：添加了示例图片。这里的不变量是什么，但对我来说重要的是为什么。

标签： javaclassinvariants

Answer 1

不幸的是，没有系统的方法来查看一段代码并计算出它的不变量。一种技术是考虑实例状态可能无效的方式，然后检查这些方式是否不会发生；在这种情况下，使状态“有效”的每条规则都是不变量。但是你需要使用直觉和经验来做到这一点。

对于您的示例，此类有两个不变量：

• 堆栈仅包含 1 到 10 范围内的整数（包括 1 到 10）。
• 堆栈底部的元素是整数 5。

可以直接验证构造函数是否建立了两个不变量，并且该addCard方法保留了它们：

• 构造函数只添加范围内的数字 5，addCard如果它们在范围内，则仅将数字添加到堆栈中。
• 数字永远不会从堆栈中删除，并且数字只会添加到堆栈顶部，因此堆栈底部的 5（由构造函数放在那里）将留在堆栈底部。

重要的是要注意构造函数和addCard方法是改变实例状态或其堆栈的仅有的两种方式，因此我们不必检查任何其他代码是否保留了不变量。如果堆栈不是private，那么它会有所不同；其他代码将能够将超出范围（或null）的数字放入堆栈，或者其他代码可以从堆栈底部删除 5。