不变性

不变量

不变量是一种属性，它在程序运行的时候总是一种状态，而不变性就是其中的一种：一旦一个不变类型的对象被创建，它总是代表一个不变的值。当一个ADT能够确保它内部的不变量恒定不变（不受使用者/外部影响），我们就说这个ADT保护/保留自己的不变量.

当一个ADT保护/保留自己的不变量时，对代码的分析会变得更简单。例如，你能够依赖字符串不变性的特点，在分析的时候跳过那些关于字符串的代码；或者当你尝试基于字符串建立其他的不变量的时候，也会变得更简单。

ADT的不变性

好的ADT最重要属性是保持其不变性。
在程序运行过程中，程序始终保持不变的性质，不可变就是不可变类型的重要不变性。ADT自身有责任确保其不变性，而不是依赖于调用者或者其他模块 。

/*** This immutable data type represents a tweet from Twitter.*/
public class Tweet {public String author;public String text;public Date timestamp;/*** Make a Tweet.* @param author    Twitter user who wrote the tweet* @param text      text of the tweet* @param timestamp date/time when the tweet was sent*/public Tweet(String author, String text, Date timestamp) {this.author = author;this.text = text;this.timestamp = timestamp;}
}

我们应该怎么样做才能确保Tweet对象是不可变的（一旦被创建，author, message, 和 date都不能被改变）？
第一个威胁就是使用者可以直接访问Tweet内部的数据，例如：

Tweet t = new Tweet("justinbieber", "Thanks to all those beliebers out there inspiring me every day", new Date());
t.author = "rbmllr";

这就是一个表示暴露（Rep exposure）的例子，就是说类外部的代码可以直接修改类内部存储的数据。上面的表示暴露不仅影响到了不变量，也影响到了表示独立性，如果我们改变类内部数据的表示方法，使用者也会受到影响。
然而我们可以经过一些修饰：

    private final String author;private final String text;private final Date timestamp;

其中， private 表示这个区域只能由同类进行访问；而final确保了该变量的索引不会被更改，对于不可变的类型来说，就是确保了变量的值不可变。
但是这并没有解决全部问题，表示还是会暴露：

/** @return a tweet that retweets t, one hour later*/
public static Tweet retweetLater(Tweet t) {Date d = t.getTimestamp();d.setHours(d.getHours()+1);return new Tweet("rbmllr", t.getText(), d);
}

retweetLater 希望接受一个Tweet对象然后修改Date后返回一个新的Tweet对象。
问题出在哪里呢？其中的 getTimestamp 调用返回一个一样的Date对象，它会被 t.t.timestamp 和 d 同时索引。所以当我们调用 d.setHours()后，t也会受到影响，如下图所示：

这样，Tweet的不变性就被破坏了。这里的问题就在于Tweet将自己内部对于可变对象的索引“泄露”了出来，因此整个对象都变成可变的了，使用者在使用时也容易造成隐秘的bug。
我们可以通过防御性拷贝：

public Date getTimestamp() {return new Date(timestamp.getTime());
}

可变类型通常都有一个专门用来复制的构造者，你可以通过它产生一个一模一样的复制对象。在上面的例子中，Date的复制构造者就接受了一个timestamp值，然后产生了一个新的对象。另一个复制可变对象的方法是使用clone()来弥补这个问题：在返回的时候复制一个新的对象而不会返回原对象的索引。
总的来说，你要特别注意ADT操作中的参数和返回值。如果它们之中有可变类型的对象，确保你的代码没有直接使用索引或者直接返回索引。

表示不变量和抽象函数

在研究抽象类型的时候，先思考一下两个值域之间的关系：

表示域（space of representation values）

里面包含的是值具体的实现实体。在简单的情况下，一个抽象类型只需要实现为单个的对象，但是更常见的情况是使用一个很多对象的网络。

抽象域（space of abstract values）

里面包含的则是类型设计时支持使用的值。这些值是由表示域“抽象/想象”出来的，也是使用者关注的。例如，一个无限整数对象的抽象域是整个整数域，但是它的实现域可能是一个由原始整数类型（有限）组成的数组实现的，而使用者只关注抽象域。
但是，实现者是非常“在意”表示域（和抽象域）的，因为实现者的责任就是实现表示域到抽象域的转换（映射）。

例如，我们选择用字符串来表示一个字符集合：

public class CharSet {private String s;...
}

如上图所示，表示域R包含的是我们的实现实体（字符串），而抽象域里面是抽象类型表示的字符集合，我们用箭头表示这两个域之间的映射关系。这里要注意几点：

1.每一个抽象值都是由表示值映射而来 。我们之前说过实现抽象类型的意义在于支持对于抽象值的操作，即我们需要能够创建和管理所有的抽象值，因此它们也必须是可表示的。
2.一些抽象值是被多个表示值映射而来的。这是因为表示方法并不是固定的，我们可以灵活的表示一个抽象值。
3.不是所有的表示值都能映射到抽象域中。在上面这个例子中，“abbc”就没有被映射。因为我们已经确定了表示值的字符串中不能含有重复的字符——这样我们的 remove 方法就能在遇到第一个对应字符的时候停止，因为我们知道没有重复的字符。

由于我们不可能对每一个映射一一解释，为了描述这种对应关系和这两个域，我们再定义两个概念：

抽象函数abstraction function

是表示值到其对应的抽象值的映射：
AF : R → A
快照图中的箭头表示的就是抽象函数，可以看出，这种映射是满射，但不一定是单射（不一定是双射）。

表示不变量rep invariant

是表示值到布尔值的映射：
RI : R → boolean
对于表示值r，当且仅当r被AF映射到了A，RI®为真。换句话说，RI告诉了我们哪些表示值是“好”的（能够去表示A中的抽象值），在下图中，绿色表示的就是RI®为真的部分，AF只在这个子集上有定义。

例如上图中，CharSet这种类型的实现禁止有重复字符，所以 RI(“a”) = true, RI(“ac”) = true, RI(“acb”) = true, 但是 RI(“aa”) = false, RI(“abbc”) = false.其中为假的集合用红色区域表示，合法的（为真）的字符串集合用绿色表示。
表示不变量和抽象函数都应该在表示声明后注释出来：

public class CharSet {private String s;// Rep invariant://   s contains no repeated characters// Abstraction function://   AF(s) = {s[i] | 0 <= i < s.length()}...
}

不同的内部表示，需要设计不同的 AF 和 RI
选择某种特定的表示方式 R ，进而指定某个子集是“合法”的 ( RI)，并为该子集中的每个值做出“解释 ”(AF) 即如何映射到抽象空间中的值。

即使是同样的抽象域和表示域以及同样的表示不变量，我们也可能有不同的解释方法/抽象函数。还是上面的例子，我们可以对表示值中相邻的字符做不同的解释： “acgg” 被解释为[a-c] 和 [g-g]中的字符，即{a,b,c,g}。现在的映射如下图所示：

public class CharSet {private String s;// Rep invariant://   s.length() is even//   s[0] <= s[1] <= ... <= s[s.length()-1]// Abstraction function://   AF(s) = union of { c | s[2i] <= c <= s[2i+1] } //           for all 0 <= i < s.length()/2...
}

总之，一个ADT的实现不仅是选择表示域（规格说明）和抽象域（具体实现），同时也要决定哪一些表示值是合法的（表示不变量），合法表示会被怎么解释/映射（抽象函数）。

检查表示不变量

表示不变量不仅是一个简洁的数学概念，你还可以通过断言检查它的不变属性来动态捕捉bug。例如上面的RatNum，这里就举出了一种检查的方法：

// Check that the rep invariant is true
// *** Warning: this does nothing unless you turn on assertion checking
// by passing -enableassertions to Java
private void checkRep() {assert denominator > 0;assert gcd(Math.abs(numerator), denominator) == 1;
}

你应该在每一个创建或者改变表示数据的操作后调用 checkRep() 检查不变量，换句话说，就是在使用创建者、生产者以及改造者之后。在上面的RatNum中，你可以看到我们在两个创建者的最后都使用了 checkRep() 进行检查。

虽然说观察者通常不需要使用 checkRep() 进行检查，但这也是一个不错的主意。因为在每一个操作中调用 checkRep() 检查不变量更能够帮助你捕捉因为表示暴露而带来的bug。

AF, RI以及表示暴露安全性的注解

你应该在抽象类型（私有的）表示声明后写上对于抽象函数和表示不变量的注解，这是一个好的实践要求。
当你在描述抽象函数和表示不变量的时候，注意要清晰明确：
1.对于RI（表示不变量），仅仅宽泛的说什么区域是合法的并不够，你还应该说明是什么使得它合法/不合法。
2.对于AF（抽象函数）来说，仅仅宽泛的说抽象域表示了什么并不够。抽象函数的作用是规定合法的表示值会如何被解释到抽象域。作为一个函数，我们应该清晰的知道从一个输入到一个输入是怎么对应的。
3.还需要将表示暴露的安全性注释出来。这种注释应该说明表示的每一部分，它们为什么不会发生表示暴露，特别是处理的表示的参数输入和返回部分（这也是表示暴露发生的位置）。

这样做的意义即给出理由，证明代码并未对外泄露其内部表示——自证清白

一个ADT的规格说明应该写什么？

如上图所示，规格说明在使用者和实现者之间构建起了一道“防火墙”。抽象类型的规格说明（包含操作的说明）应该只关注使用者可见的部分，这包括参数、返回值、可能抛出的异常。例如规格说明需要引用T的值时，它应该是抽象域的值而非表示域。

规格说明不应该谈论具体的表示/实现细节，例如表示域里面的值。它应该认为表示本身（私有区域）对于使用者是不可见的，就像是方法里面的局部变量对外部不可见。这也是为什么我们在注解表示不变量和抽象函数的时候使用的是"\"注释而非典型的Javadoc格式。如果我们使用Javadoc注释的话，内部的实现细节会出现在规格说明中，而这会影响表示独立性以及信息隐藏。

用ADT不变量替换前置条件

良好设计的ADT的一个大优点在于我们可以使用它将本该写在前置条件中的限制封装起来。例如，现在有一个规格说明是这样：

/** * @param set1 is a sorted set of characters with no repeats* @param set2 is likewise* @return characters that appear in one set but not the other,*  in sorted order with no repeats */
static String exclusiveOr(String set1, String set2);

我们可以利用ADT（SortedSet）的不变量属性要求这种前置条件：

/** @return characters that appear in one set but not the other */
static SortedSet<Character> exclusiveOr(SortedSet<Character>  set1, SortedSet<Character> set2);

这满足了我们所有的要求：
1、远离bug：因为要求的条件（排序、无重复）都已经是ADT的不变量了，所以Java可以对其进行静态检查，在编译期阻止所有不满足的操作。
2、易于理解：因为这样写更简单，并且ADT SortedSet 的名字就已经表明了它该有的属性。
3、可改动：因为我们可以改变 SortedSet 的内部实现而不影响 exclusiveOr 或其他的使用者代码。

如何建立不变量

不变量是一种在程序中一直为真的属性，对于对象而言，就是从对象创建开始一直具有的属性。
为了保持一个不变量，我们需要：
1.确保在对象创建的时候不变量成立
2.确保对对象在接下来的每一个改变后不变量依然成立

1.创建者和生产者必须对新的对象就建立不变量
2.改造者和观察者必须保持/保护这种不变量
3.表示暴露会使得情况更加复杂，如果一个表示被暴露出来，那么程序的任何地方都可能对其进行修改，我们也就没法确保不变量一直成立了。所以使用不变量完整的规则应该是：
结构归纳法. 如果一个抽象数据类型的不变量满足：
被创建者或生产者创建；被改造者和观察者保持；没有表示暴露。
那么这种类型的所有实例的不变量都是成立的。