荷兰国旗问题
荷兰国旗问题可以抽象为：给定一个含有三种颜色（蓝、白、红）的枚举数组t[n]，要求将数组元素重新排列，使得蓝白红依次处于数组段的 [0..b-1]、[b..r-1]、[r..n-1]。（验证时间约110sec）
[Back to Index]
验证特点：量化断言，逻辑函数，数组置换性的谓词描述，幽灵数组，强类型不变式
标注说明：函数前条件：利用逻辑变量记录原数组。
函数后条件：排序后的数组蓝白红依次处于数组段[0..b-1]、[b..r-1]、[r..f.n-1]。排序前后数组中各色元素的个数不变，即保持置换性。
程序样例 
