属性测试生成与收缩

功能说明

该示例演示属性测试中的收缩思路：先给定一个违反属性的输入，再系统性地删除元素，只要仍违反属性就保留删除结果，直到无法再删。最终得到的最小反例比随机失败用例更易读，也更容易看出属性为何不成立。check 表示“应为非递减”的属性。

关键代码

shrink 外层循环在每轮尝试删除一个元素，只要属性仍失败即接受该候选并重新开始扫描，直到一整轮都无法删除为止。holds 是返回布尔谓词的注入函数，使收缩逻辑与具体属性解耦。findCounterexample 先判定初始输入是否已经失败，失败则进入收缩，否则报告没有反例。最终保留的反例长度最小且不含冗余元素。

使用注意

这是一个教学用的最小收缩器，只按删除做收缩，真实工具还会收缩数值本身（向零、向边界逼近），对本例这种顺序属性，数值收缩同样必要。收缩必须保证候选确实仍违反属性，否则会返回一个通过的例子。谓词应快速且无副作用，因为收缩会多次调用它；对昂贵谓词应缓存结果。删除策略的复杂度为平方级，元素极多时需改用更高效的收缩算法。

代码示例

export interface PropertyCase { readonly numbers: number[]; }

export function check(numbers: number[]): boolean {
  return numbers.every((n, i) => i === 0 || (numbers[i - 1] as number) <= n);
}

export function shrink(failing: number[], holds: (input: number[]) => boolean): number[] {
  let current = failing;
  let changed = true;
  while (changed) {
    changed = false;
    for (let i = 0; i < current.length; i++) {
      const candidate = current.filter((_, index) => index !== i);
      if (!holds(candidate)) {
        current = candidate;
        changed = true;
        break;
      }
    }
  }
  return current;
}

export function findCounterexample(seed: number[], holds: (input: number[]) => boolean): number[] | null {
  if (!holds(seed)) return shrink(seed, holds);
  return null;
}